[isabelle-dev] Isabelle/jEdit feedback
makarius at sketis.net
Mon Mar 19 16:20:58 CET 2012
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
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.
More information about the isabelle-dev