[isabelle-dev] Isabelle/jEdit feedback
c-sterna at jaist.ac.jp
Fri Mar 16 14:48:25 CET 2012
Thanks for the effort put into jEdit! With every revision I use it more
frequently and for ever larger developments. I already reached the point
where I am annoyed when I have to fall back to ProofGeneral (glaring at
the Screen for some moments and waiting for a result, until I figure
that I first have to indicate a "next" ...).
I also have an innocent "feature request". After I typed something in
Isabelle/jEdit I have to move the cursor in order to get the
corresponding output. EDIT: just while trying some examples, I noticed
that this is actually not always the case. Sometimes jEdit behaves
exactly as I wish... I did not yet find out what makes the difference.
Btw: I am using changeset 9ff441f295c2 of Isabelle and jedit_build-20120313.
Anyway. To make myself more clear, here are two examples ("|" indicates
the cursor position) where it did not behave as desired (by me ;)).
lemma "A = A"|
previous output is active. When cursor is moved to the left I get the
expected goal message.
Again, I have to move the cursor to the left to get the output of
PS: In jEdit when finishing a proof one does not get the resulting
theorem in the output (in contrast to ProofGeneral). Is there a special
reason why not? If not, could this be added?
More information about the isabelle-dev