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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
