Re: [isabelle] Isabelle2014-RC0: symbol completion in antiquotations

On Tue, 8 Jul 2014, Andreas Lochbihler wrote:

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>.

In June I wrote a very long section on Completion for the Isabelle/jEdit manual. It might or might not shed light on this, and I would be interested to get feedback about the text.

The problem seen here is one of "language context" in the completion mechanism. In certain situations, a \foo sequence is syntactically invalid and destroys the intended language context, dropping out of the syntax of a certain sub-language. Thus the "symbols" flag of the language might get lost, and symbols are not completed.

I have presently no better answer than using a valid \<foo> symbol and complete on that.

Note that the problem would be absent, if the traditional quotes were replaced by the more robust cartouches. But this is a bit speculative at the moment.

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

The general intention of completion is to provide a "Do what I mean" mechanism for the Prover IDE, but the more it advances and becomes smarter, the more surprising the breakdowns.

For the moment we should just continue collecting observations, and further hints how to work smoothly with the system as it is now.


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