Isabelle can send "active markup" from ML in the output panel to e.g. suggest proof outlines when typing
This is a nice feature but it is slightly annoying to have to click on the text for it to be inserted.
Is there any possibility to bind this functionality to a keyboard shortcut, e.g. by writing a piece of Scala code (I have never used Isabelle/Scala and I cannot find anything in the list of the "Isabelle plugin" default shortcuts in Isabelle/jEdit)?
Yes, you'll have to build a custom jEdit action and bind it to a shortcut. The
goto-entity functionality would be a good example of something like that.
Last updated: Aug 15 2022 at 02:13 UTC