Stream: General

Topic: Shortcut to complete "active markup"

view this post on Zulip 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)?

view this post on Zulip 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 07 2023 at 08:19 UTC