[isabelle-dev] Sledgehammer proof text insertion
makarius at sketis.net
Tue Sep 24 22:36:04 CEST 2013
On Thu, 5 Sep 2013, Lars Noschinski wrote:
> On 05.09.2013 13:35, Florian Haftmann wrote:
>> after some time playing around with the new sledgehammer panel
>> (ab4edf89992f), here my feedback:
> Regarding this (and also the new Find panel), I would like to see a keyboard
> shortcut, not only to open the panel (those can already be defined), but to
> select the major function of the panel, i.e.
> start sledgehammer for the sledgehammer panel
> give focus to the search term input box for the find panel.
I've made several refinements, including the usual Mac OS X add-ons after
everything seems finished (104a08c2be9f etc.).
The jedit actions isabelle.find-panel and isabelle.sledegehammer-panel
should popup these panels, and give focus according to normal jEdit window
manager rules, unless prevented by operating system window manager rules.
Also note that the little action command line (C+ENTER) of jEdit has
built-in completion via TAB. (Unfortunately that important jEdit
functionality is presently broken for Mac OS X, probably due to some
strange GUI focus effects, that are independent of the focus stuff I've
jEdit actions can be bound to keyboard shortcuts, menus etc. In jEdit
such things are normally not done by default, since the keyboard space is
relatively limited -- this is not ESCAPE-META-ALT-CONTROL-SHIFT. (We have
even some pending problems with important key sequences like COMMAND-comma
on Mac OS X that need be be remapped, since it clashes with standard
Preferences functionality according to Apple. I did not find a reasonable
free slot on the intersection of English / German / French keyboard yet.
Another open problem is how to reconcile the recent split into several
default keymaps -- every jEdit developer now seems to have his very own.)
More information about the isabelle-dev