[isabelle-dev] jedit

[Makarius]

On Wed, 16 May 2012, Lawrence Paulson wrote:

> A quirk of the current setup is that typing “sledgehammer" has no 
> effect; you have to explicitly move the cursor after this keyword before 
> sledgehammer launches. A menu would solve this problem as well.

I don't see what you mean.  In Isabelle2012-RC2 I can type "sl", wait 
300ms, press RETURN, and see sledgehammer running and producing Output 
incrementally.  Then I can click on one of the proposed metis proofs to 
replace the inlined command by the result -- this was an idea of Alex 
Krauss to make it work easily without further ado.

You should be able to use existing jEdit abbreviations or macro mechanisms 
to turn this into a single key or menu invocation, but I am not really an 
expert of this so far.  jEdit also has quite good documentation.


 	Makarius