Email Gateway (Aug 19 2022 at 15:08): Email Gateway (Aug 19 2022 at 15:08):From: Peter Lammich <lammich@in.tum.de>
Hi List.
Refering to Isabelle/jedit 2014-RC1:
How can I define shortcuts for actions in general, and, in particular,
for the action of clicking "Update" in the output panel.
This action does not occur as "command" in jedit's shortcut menu, nor
does the "action bar" mention it, nor does macro-recording work for it.
So I have no clue where to start.
Email Gateway (Aug 19 2022 at 15:09):From: Makarius <makarius@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
Email Gateway (Aug 19 2022 at 15:12):From: Fabian Immler <immler@in.tum.de>
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
Email Gateway (Aug 19 2022 at 15:12):From: Carst Tankink <carst.tankink@inria.fr>
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">
<CODE>
wm.addDockableWindow("isabelle-output");
wm.getDockableWindow("isabelle-output").update_now();
</CODE>
</ACTION>
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.
Carst
Email Gateway (Aug 19 2022 at 15:41):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 20 2024 at 04:19 UTC