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

Hi Makarius,

On 09/07/14 17:27, Makarius 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.
I read the text on completion, but I must admit that I would not have been able to figure out your explanation with dropping out of the language context. As is usual in the Isabelle documentation, your text describes the general principles, but not the concrete instances that one encounters in practice. For example, I was not able to figure out which language contexts exist (in a plain Isabelle/HOL session) and when language contexts are switched.

There probably are the contexts "outer syntax", "inner syntax", "LaTeX text", ML source, but there could also be something like "inner syntax inside the antiquotation text" which might behave differently from "inner syntax inside the antiquotation term" and "inner syntax inside the antiquotation const". I don't know how I could find out which language context I am currently working in. Maybe it suffices to display the language context of the curser somewhere in Isabelle (e.g., in the status bar as Emacs used to do it).

I remember a presentation you gave long ago (possibly at the workshop in Cambridge in 2010) in which you showed that you can nest an term antiquotation inside an ML antiquotation inside ... inside a text block. That made me think that there is probably not one separate language context for each antiquotation, but that I might expect the same behaviour as with normal inner syntax.


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.