[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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