Email Gateway (Aug 19 2022 at 14:50): Email Gateway (Aug 19 2022 at 14:50):From: Makarius <makarius@sketis.net>
There are many fine points like that, which I would have liked to see in
forthcoming Isabelle2014, but did not make it due to still existing
baggage of Proof General legacy.
Maybe after next week at Vienna we have a better impression how many
remaining uses of Proof General are left over (as well as remaining
users).
Everyone is invited to discuss that not just with me, but with any of the
Isabelle/jEdit veterans. Early adopters have jumped on the train in
October 2011 with the first stable release of the Prover IDE, and the
coming one is already version 5 in the internal counting.
Makarius
Email Gateway (Aug 19 2022 at 15:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 15:16):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 19 2022 at 15:17):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.
Andreas
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.Makarius
Email Gateway (Aug 19 2022 at 15:18):From: Makarius <makarius@sketis.net>
This is done with the ubiquitious C-hover idiom: it produces a popup
saying "language: NAME". The other flags for the language are not
printed, but accessible dynamically in SideKick with "isabelle-markup"
parser in the status window:
<language name="NAME" symbols="false" antiquotes="false" delimited="true"/>
Or you look in ~~/src/Pure/PIDE/markup.ML for the language contexts that
are presently used in Isabelle/Pure -- but tools could invent their own.
To make this exploration more fun, consider this formal Isar source:
text ‹ see @{file "~~/src/Pure/PIDE/markup.ML"} ›
Here the file-system path specification has language context "path",
because the "file" antiquotation has provided that semantic information.
This means that file-name completion is active in PIDE: you can type some
prefix of it and use C+b to get more from the directory content.
If this is madness, there is method in it ...
Makarius
Email Gateway (Aug 19 2022 at 15:19):From: Christian Sternagel <c.sternagel@gmail.com>
Does that mean that cartouches for antiquotations will not be part of
Isabelle2014? Just for the record: I would like to have
@{term ‹α something›}
since, as you said, this would avoid some problems with symbol completion.
cheers
chris
Last updated: Nov 21 2024 at 12:39 UTC