[isabelle-dev] Isabelle/jEdit feedback

[Makarius]

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