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.*;
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.


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

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