[isabelle-dev] Feedback from a Isabelle tutorial
krauss at in.tum.de
Fri Jun 24 22:01:14 CEST 2011
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
> 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
More information about the isabelle-dev