On Fri, 16 Mar 2012, Christian Sternagel wrote:
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.
I've tried it briefly in 9ff441f295c2, but could not reproduce the problem
on the spot.
Generally, the concept of relating the Output focus via cursor movements
is a bit odd, and the implementation fragile. I've recently refined the
command spans to include any trailing whitespace, so d68ea01d5084 could
discontinue the backward movement towards the next proper command for
output. In 9ff441f295c2 this should have done the job, but there might
have been some fragmentation of command spans do to the sequence of edits
leading to the text.
I keep on refining this ...
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?
Proof General spends most of the time parsing or printing. In the
Isabelle/Scala document model the tendency is to reduce that by default,
running essentially in batch mode. Practically, there are still many
situations where too much is printed (bad reactivity of the Prover IDE for
really big sessions) or too little.
Proper management of additional diagnostic output over existing command
evaluation still needs to be added. It will cover printing of goal
states, results, add-ons like auto quickcheck etc.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
