Re: [isabelle] Remaining reasons for Proof General
On Tue, 12 Nov 2013, Joachim Breitner wrote:
I believe that that will soon enter your procedural memory. I also just
recently switched on this feature and from time to time write Γma, but
it becomes less often quickly. With this, entering fancy symbols becomes
That is sophistication level 1.
There is still the problem that it relies on unique completions, and
some symbols don’t have short unique prefixes, e.g. \sqsubsete is not a
great win – but then, this symbol has [=, so I just have to get used to
At sophistication level 2 you can experiment with your own symbol
abbreviations, by imitating / overriding some entries of
$ISABELLE_HOME/etc/symbols with your own entries in
There is an art to make certain groups of symbols non-unique on purpose to
provoke a popup, while others are unique for immediate insertion.
I've played this game at the end of the summer, until I was myself
satisfied with 2-3 rounds of refinement. In the whole history of Isabelle
and Proof General, I have never been that fast typing certain formal
texts. Even more brevity and immediacity of completion is conceivable,
but my next priority is to make context-sensitive completion based on
information by the prover.
I had some concrete ideas how to approach this delicate problem at the end
of the summer, but then got stuck with too many GUI reactivity problems.
You have seen the last bits of that with the key event loss at extreme
typing speed. (Next time I simply avoid switching GUI focus for
completion; it will only require the usual 2-3 weeks of testing to
This archive was generated by a fusion of
Pipermail (Mailman edition) and