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?
@Fabian Huch @Yecine Megdiche
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
.
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
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
).
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)
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.
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: Dec 07 2024 at 16:22 UTC