[isabelle-dev] Feedback from a Isabelle tutorial
makarius at sketis.net
Sat Jun 25 10:55:48 CEST 2011
On Fri, 24 Jun 2011, Alexander Krauss wrote:
> Another instance, which comes up in an exploratory/teaching context, is the
> following scenario:
> lemma "x = y" -- some false conjecture
> try -- see if it "works"
> ^ -> counterexample found immediately
> cursor is here
> At this point I would like to go up and correct the lemma, but I cannot,
> since the editor suggests "try_methods" as a completion of "try". I have to
> press escape first.
> Of course, in an ideal world, I would not have to type "try" in the first
> place, but currently this is our way of working.
> Suggestion: Simply kill completion of commands (not symbols)???
The inlining of diagnostic commands into the text is awkward in several
ways. There should be a completely different way to do it, without
intruding the text area in the first place.
In general the command language is designed to have completion of some
form. This explains the relatively long and explicit command names, e.g.
"definition", "theorem" instead of cryptic abbreviations. The physical
mechanism to be used is a different question. jEdit alone has about 5
such mechanisms as part of the main editor framework or plugins, and in
the greater Java/Swing world there are some more such frameworks.
What you see right now is the builtin auto-completion of jEdit/Sidekick.
The regular jEdit completion/abbreviation mechanism needs to be requested
explicitly by certain command sequences, and it is not configured by
One needs to make a market survey to find really good mechanisms that do
not intrude the editing process (as in newer Proof General versions, for
More information about the isabelle-dev