[isabelle-dev] Isabelle/jEdit feedback

[Christian Sternagel]

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?