Dear Makarius,
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.
find_theorems "wf"|
Again, I have to move the cursor to the left to get the output of
find_theorems.
cheers
chris
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?
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
