[isabelle-dev] Sledgehammer proof text insertion

[Makarius]

On Thu, 5 Sep 2013, Lars Noschinski wrote:

> On 05.09.2013 13:35, Florian Haftmann wrote:
>> Hi,
>> 
>> 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
>
> and
>
>  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 
done elsewhere.)

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.)


 	Makarius