Re: [isabelle] Defining Shortcut for Output-Panel: Update
You could use a BeanShell macro which emulates clicking on "Update", e.g. as follows:
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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and