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

The following works, but I am not sure if I missed corner cases:

- Add the following method to src/Tools/jEdit/src/output_dockable.scala:

  def update_now() { handle_update(true, None) }

- Add the following snippet to src/Tools/jEdit/src/actions.xml:

  <ACTION NAME="isabelle.update_output">

- Add the following to src/Tools/jEdit/src/jEdit.props (Isabelle.props probably works as well):

  isabelle.update_output.label=Update output window

Recompile and repackage jEdit, obviously.
This will actually open the output dockable if it is not yet open, removing the addDockableWindow call would prevent this behaviour.


On 07/30/2014 09:32 PM, Makarius wrote:
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 MHonArc.