[isabelle] Active Area for jEdit Console



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.

--
Dr. Simon Foster - Lecturer in Computer Science
RoboStar Group, University of York

My normal working hours are 8:30am to 4:30pm Monday to Friday.
java.lang.NullPointerException: Cannot invoke "org.gjt.sp.jedit.EditAction.noRememberLast()" because "action" is null
	at org.gjt.sp.jedit.gui.InputHandler.invokeAction(InputHandler.java:326)
	at org.gjt.sp.jedit.gui.InputHandler.invokeAction(InputHandler.java:308)
	at isabelle.jedit.Active$Misc_Handler.$anonfun$handle$4(active.scala:71)
	at isabelle.GUI_Thread$.later(gui_thread.scala:44)
	at isabelle.jedit.Active$Misc_Handler.handle(active.scala:71)
	at isabelle.jedit.Active$.$anonfun$action$3(active.scala:36)
	at isabelle.jedit.Active$.$anonfun$action$3$adapted(active.scala:36)
	at scala.collection.immutable.List.find(List.scala:413)
	at isabelle.jedit.Active$.$anonfun$action$2(active.scala:36)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at isabelle.jedit.Rich_Text_Area.robust_body(rich_text_area.scala:49)
	at isabelle.jedit.Active$.action(active.scala:33)
	at isabelle.jedit.Rich_Text_Area$$anon$5.$anonfun$mouseClicked$1(rich_text_area.scala:230)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at isabelle.jedit.Rich_Text_Area.robust_body(rich_text_area.scala:49)
	at isabelle.jedit.Rich_Text_Area$$anon$5.mouseClicked(rich_text_area.scala:214)
	at java.desktop/java.awt.AWTEventMulticaster.mouseClicked(AWTEventMulticaster.java:278)
	at java.desktop/java.awt.AWTEventMulticaster.mouseClicked(AWTEventMulticaster.java:277)
	at java.desktop/java.awt.Component.processMouseEvent(Component.java:6617)
	at java.desktop/javax.swing.JComponent.processMouseEvent(JComponent.java:3342)
	at java.desktop/java.awt.Component.processEvent(Component.java:6379)
	at java.desktop/java.awt.Container.processEvent(Container.java:2263)
	at java.desktop/java.awt.Component.dispatchEventImpl(Component.java:4990)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4822)
	at java.desktop/java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4919)
	at java.desktop/java.awt.LightweightDispatcher.processMouseEvent(Container.java:4557)
	at java.desktop/java.awt.LightweightDispatcher.dispatchEvent(Container.java:4489)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2307)
	at java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2769)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4822)
	at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:772)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:715)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:391)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:745)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:743)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:391)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
	at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:742)
	at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
	at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.