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