[isabelle-dev] jEdit

[Christian Sternagel]

Dear Makarius,

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?

cheers

chris