makarius at sketis.net
Wed May 16 16:01:03 CEST 2012
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.
More information about the isabelle-dev