Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Active Area for jEdit Console

view this post on Zulip Email Gateway (Jun 21 2021 at 09:10):

From: Simon Foster via Cl-isabelle-users <>
Hello everyone.

I'm currently trying to implement an active area in Isabelle/jEdit that
would allow me to open an instance of the jEdit console to interpret a file
produced by the code generator. The workflow I'd like to achieve is that
the user enters an Isabelle command into a theory (analogous to
export_code), which runs the code generator and then produces an active
area in the Output pane with a link that opens the file produced in, say,

I've looked at Pure/PIDE/Active.ML and I can see this allows sending markup
to PIDE for interpretation. As far as I can see there is currently a
limited number of active area types that can be created, such as "brower",
"theory_exports" etc.

One way to achieve opening a console is to use a jEdit action via
"jedit_action". The console plugin provides "runInSystemShell(view,
command)", which implements almost the functionality needed. I can indeed
execute the command via BeanScript in jEdit. I've then tried to create a
new jEdit action, by adding the following lines
to src/Tools/jEdit/src/actions.xml:

<ACTION NAME="ghci">
runInSystemShell(view, "ghci");

However, whilst jEdit recognises the new action on startup, and it can be
called using JEdit.check_action ("ghci", @{here}), when executed I get the
error "java.lang.NullPointerException: Cannot invoke
"org.gjt.sp.jedit.EditAction.noRememberLast()" because "action" is null"
(see attached). It doesn't matter what I put in the ghci action code, it
always produces the same error. I presume that I've not added the jEdit
action in the correct way.

How can I fix this error? Is there a better way of achieving this workflow?
Any help would be appreciated.



Last updated: Jul 15 2022 at 23:21 UTC