Re: [isabelle] Defining Shortcut for Output-Panel: Update



Hi Peter,

You could use a BeanShell macro which emulates clicking on "Update", e.g. as follows:

import isabelle.jedit.*;
setAccessibility(true);
output = Isabelle.output_dockable(view);
if (output.isDefined()) output.get().update.doClick();

Then bind this macro to a shortcut, but I suppose the clicking-emulation could be made an action as well.

Fabian



Am 30.07.2014 um 21:32 schrieb Makarius <makarius at sketis.net>:

> On Wed, 30 Jul 2014, Peter Lammich wrote:
> 
>> Refering to Isabelle/jedit 2014-RC1:
>> 
>> How can I define shortcuts for actions in general
> 
> The Isabelle/jEdit manual briefly mentions that, and refers to the original jEdit documentation for further information.  Both are accessible in the Documentation panel.
> 
> 
>> in particular, for the action of clicking "Update" in the output panel.
> 
> That is not an action, so it cannot be bound to shortcuts etc.  I can't say on the spot if it could be made an action with reasonable effort.
> 
> 
> 	Makarius
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.