Simon Wimmer (Mar 01 2022 at 13:59): Simon Wimmer (Mar 01 2022 at 13:59):Isabelle can send "active markup" from ML in the output panel to e.g. suggest proof outlines when typing proof cases/proof induction.
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)?
Fabian Huch (Mar 03 2022 at 13:59):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: Dec 21 2024 at 12:33 UTC