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



On Thu, 31 Jul 2014, Fabian Immler wrote:

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.

Excellent. I am impressed by the flexibility of jEdit and BeanShell in particular.

Yet another very practical proof that the Java guys started out as LISP guys -- J. Gosling even had his own version of Emacs in his youth.


	Makarius




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