# [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



• Follow-Ups:

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