[isabelle-dev] Remaining uses of Proof General?

[Andreas Lochbihler]

Hi Makarius,


On 28/04/14 23:10, Makarius 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.
>
> 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.
My completion delay is 0.1. When writing Isabelle terms normally, this is the amount of 
time that does not break my flow of typing.

> 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.
But this correct nesting is exactly the problem. When I type \un while writing the above, 
the closing parenthesis are not there yet. The prover sees something like

text {* @{term "A \un

lemma foo: "..." by ...


> What is funny is that Proof General was actually one of the main reasons of moving only
> slowly in such token language reforms.
I am glad that PG still works for most of my theories and I try to keep that state as long 
as feasible. There are already problems with new keywords declared by AFP entries that are 
not listed in the keywords file. I then usually insert ; as a delimiter. But I try to 
process such theories with jEdit and only go back to XEmacs/PG when I cannot stand 
Isabelle/jEdit any longer (which usually happens when I debug the code generator setup).

Andreas