On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
a) Given some text like
definition foo where "foo = ..."
when I add an attribute like [simp]: after the where, I get a symbol
completion popup to replace the : with the element sign. Usually, my
next thing is to move the cursor with the cursor keys. But the popup
gobbles all the key strokes until I explicitly close it with ESC. As
colons are used everywhere in Isabelle's outer syntax, it would really
be great if the popup only appears when I am in inner syntax.
b) Sometimes, when I write a HOL term, I used to not get the completion
popup when I enter something like \un if there were sufficiently many
parse errors in that partial term. Even Ctrl-b did not help. However, I
cannot reproduce it in a small example at the moment.
We should move anything concerning completion on specific threads on this
mailing list, with explicit subject what it is about. It will take quite
some time for the coming release to stabilize in that respect. There are
a bit too many ambitious and smart mechanisms involved here.
For now just a few notes.
In the case a), I guess that you still have the completion delay 0.0,
while I presently work with 0.5 to give the prover a chance to add
semantic completion information, before any popups are shown. That
includes a "no_completion" markup produced by the prover, specifically for
things like ":", although this introduces a real danger of
non-determinism.
The gobbling of key events by the popup should not happen, but there are
some uncertainties due to key event workarounds in jEdit, and workarounds
around these in Isabelle/jEdit. The basic idea is that the popup consumes
exactly those key strokes that are relevant to it, and passes everything
else to the main text area -- this is also what jEdit usually does. This
behaviour has fluctuated concerning cursor left and right keys several
times, and I need to check this once again soon.
For current 9c3f0ae99532 I confirm that the first cursor left/right event
is indeed absorbed.
Case b) with \foo sequences happens whenever there is some semantic
completion context and string literals involved: backslash sequences
destroy the string token, and thus may change the context again. Here is
an example:
text {*
@{term "A \un B"}
*}
The language context for 'text' disables symbol completion, because it is
in conflict with latex macros, as just seen on the thread on
isabelle-users "Symbol Shortcuts vs. LaTeX code". The antiquotation
changes the language context again to allow symbols, but the malformed
string "A \un B" breaks that, and it falls back into the enclosing text
context. So the \un cannot be completed.
One of the motivations for backslash escapes is to make them different
from usual legal input, but exactly that causes the problems here. I have
started to think about making bad string tokens more acceptable to certain
language layers, but that is once again an extra complication.
A different approach is to use new cartouche syntax instead, which
addresses old issues of quotation robustness and escape confusion
uniformly. Using that token syntax, the above example becomes this:
text ‹
@{term ‹A \un B›}
›
Here the \un works as expected -- the cartouche remains intact
independently of its content, as long as the funny parentheses are nested
properly. There is a different error, though: the term parser does not
accept outer cartouche tokens yet. It could allow that, but I found this
too ambitious as a start for the new syntax.
What is funny is that Proof General was actually one of the main reasons
of moving only slowly in such token language reforms. We are back again
in a dead-lock situation, and not the first time in the past few years.
Leaving the old Emacs world behind more decisively would free a lot of
hidden resources, and that could have been done at least 2 years ago
without any regrets.
Of course there is no fundamental problem of Proof General supporting
cartouches. There was once special code for nested comments that could be
reactivated. The point is that somebody would have to do something, and
not just expect that software magically maintains itself.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
