[isabelle-dev] Feedback from a Isabelle tutorial

[Tobias Nipkow]

Command completion needs to be context aware to work well. Otherwise it 
can indeed become a distraction.

Tobias

Am 24/06/2011 22:01, schrieb Alexander Krauss:
> Hi all,
>
> Now that this topic is already active, here is more:
>
> In a small course here at TUM
> (http://www4.in.tum.de/lehre/vorlesungen/perlen/SS11/) we are also using
> jedit exclusively for the first time, and I can confirm the observation
> that it makes it slightly easier for newbies to get started. In
> particular, the "How can I copy and paste?", "How do I open a file?"
> questions all go away, since the editor commands/key sequences are less
> obscure. There are also less installation issues (we have no virtualbox
> image, but a custom bundle, which I built from a development version).
>
> Here are two (minor) issues I noticed, which do get in the way and may
> be easy to fix:
>
> 1) Command completion: This may be one of the features that look nice
> but are useless in practice and often get in the way: Some frequent
> commands are prefixes of other rather obscure commands, which will then
> be suggested by the auto-completion: When I type "apply" and pause for a
> moment to think, the editor suggests "apply_end", which many users don't
> even know about. This steals (a) the focus, as I cannot move the cursor
> up/down at this point and (b) my attention.
>
> 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)???
>
>
> 2) Since entering non-ascii versions of arrows takes two extra
> keystrokes and some attention, students tend to just use the ascii
> variants. I don't know if this is good or bad, but when I give them a
> file for editing that has nice arrows, after editing, it usually has
> both versions, and I have to explain that they are the same. I
> principle, this could happen with PG/Emacs too, but it normally
> wouldn't, because of the automatic substitution.
>
>
>>> It is a known issue (if an issue at all) that in Isabelle/jEdit it is
>>> sometimes necessary to cut-and-paste some lines in order to
>>> "synchronize."
>
>> This behaviour is indeed getting in the way in practice. It works
>> according to the "specification" of the editing model, but
>
> What is actually the specification of the editing model? I am just
> curious here, and if you can explain it quickly, it may give me an
> intuition of what's happening when something goes "wrong" (i.e., as
> specified).
>
> Alex
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev