Email Gateway (Jun 21 2021 at 09:10): Email Gateway (Jun 21 2021 at 09:10):From: Simon Foster via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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,
GHCi.
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">
<CODE>
runInSystemShell(view, "ghci");
</CODE>
</ACTION>
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.
Regards,
Simon.
action-error.log
Last updated: Jan 04 2025 at 20:18 UTC