[isabelle-dev] Feedback from a Isabelle tutorial

[Makarius]

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

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 
example).


 	Makarius