[isabelle-dev] Feedback from a Isabelle tutorial

[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