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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
