Simon Foster (Jun 28 2021 at 09:40): Simon Foster (Jun 28 2021 at 09:40):Does anyone have any experience with "Active Areas" (e.g. sledgehammer's "Try this..." and the code generator's "See theory exports") and their interface with PIDE and jEdit? I'd like to create an active area that opens a Console in jEdit with a particular file opened. Essentially, this is to allow the direct use of an interactive command line interpreter on some files produced by the code generator. I've tried using a jEdit action (via JEdit.check_action) to do this, but it doesn't work. Anyone have any pointers?
Lukas Stevens (Jun 28 2021 at 10:56):@Fabian Huch @Yecine Megdiche
Fabian Huch (Jun 28 2021 at 11:36):If you want a dockable then you need to register the panel in src/Tools/jEdit/src/Isabelle.props, its position in src/Tools/jEdit/src/jEdit.props, and the dockable in src/Tools/jEdit/src/dockables.xml.
Lukas Stevens (Jun 28 2021 at 11:37):Fabian Huch said:
If you want a dockable then you need to register the panel in
src/Tools/jEdit/src/Isabelle.props, its position insrc/Tools/jEdit/src/jEdit.props, and the dockable insrc/Tools/jEdit/src/dockables.xml.
The question is also about how to act on clicks like with Sledgehammers Try this
Fabian Huch (Jun 28 2021 at 11:46):That is active markup (see Pure/PIDE/active.ML). You can then write a handler in Isabelle/Scala for that (see Tools/jEdit/src/active.scala).
Yecine Megdiche (Jun 28 2021 at 12:05):To act on clicks, you'd need to write a handler as Fabian explained, and register it in Tools/jEdit/src/services.xml. You can look up the Graphview_Dockable.Handler in Tools/jEdit/src/graphview_dockable.scala on an example of how to do it. It might also be a good idea to define your own markup element and add it to the list of active markups (GraphView defines Markup.GRAPHVIEW in Pure/PIDE/markup.scala, you can see where it's added and you could do the same)
Simon Foster (Jun 28 2021 at 12:27):Thank you for your very helpful answers. The functionality I need is implemented by the jEdit Console plugin in the method runInSystemShell(view, command). I noticed that there's an already an active area called "jedit_action", which presumably allows me to execute jEdit actions (cf. src/Tools/jEdit/src/actions.xml). These can apparently be implemented in BeanScript. Is there a way of implementing it this way, by an action that calls runInSystemShell? That would avoid the need to extend the PIDE Scala code, although I'm happy to do that if it's necessary.
Simon Foster (Jun 28 2021 at 14:29):I think I've figured it out myself. It is indeed possible to have an active area that calls an additional jEdit action specified in actions.xml via JEdit.check_action. It seems necessary to rebuild Isabelle/jEdit to do this.
Last updated: Jul 15 2022 at 23:21 UTC