[isabelle] Isabelle2014-RC0: symbol completion in antiquotations



Hi Makarius,

I am wondering why symbol completion in antiquotations inside text blocks behaves differently from symbol completion in ordinary term statements. Here's an example:

If I type a symbol name like \alpha in a lemma statement such as

  lemma "\alpha"

then I can tell Isabelle to replace \alpha by α. (In fact, I have enabled immediate completion, so \alp suffices.) Inside antiquotations, however, this does not seem to work.

text {* @{term "\alpha"} *} makes Isabelle complain about a "bad escape character in string". In order to get α, I now have to type \<alpha> and then press Ctrl-B. This becomes particularly annoying with longer symbol names like \<rightharpoonup>.

Is this difference intentional? I would have expected that antiquotations switch back to "inner syntax mode" and thus behave as in ordinary term statements.

Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.