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