[isabelle-dev] jEdit

[Makarius]

On Wed, 18 Apr 2012, Christian Sternagel wrote:

> it's very nice that after sledgehammer found a proof command to finish a 
> proof, I can simply click on this command in the output buffer to 
> include it in the main buffer! A slight oddity is that this merges 
> lines. E.g.,
>
>   lemma "⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys"
>   sledgehammer
>   end
>
> After sledgehammer reports
>
>   "remote_e": Try this: by (metis append_eq_conv_conj) (21 ms).
>
> In the output buffer. I click on "by (metis append_eq_conv_conj)" and 
> the result is.
>
>   lemma "⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys"
>   by (metis append_eq_conv_conj)end
>
> Maybe this could be changed such that "end" stays on its own line?

I've destroyed this recently when changing the meaning of a command span, 
to include its trailing white spans, which miraculously cuts the total 
number of command transactions in half and thus improves editing 
performance.

In Isabelle/26d0a76fef0a it should work again.  I've made further 
refinements here and in Isabelle/9980c0c094b8

So even without the long anticipated integration of "asynchronous agents" 
into the Isabelle/jEdit document model, which I had to cancel again for 
this release to take place, sledgehammer should work reasonably well.


 	Makarius