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 quite nice.

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 that.

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 $ISABELLE_HOME_USER/etc/symbols.

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 stabilize again.)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.