src/Doc/antiquote_setup.ML
changeset 57334 54c6b73774d2
parent 56467 8d7d6f17c6a7
child 57477 c3b5cb53ea79
--- a/src/Doc/antiquote_setup.ML	Mon Jun 16 20:50:56 2014 +0200
+++ b/src/Doc/antiquote_setup.ML	Mon Jun 16 21:26:50 2014 +0200
@@ -166,21 +166,32 @@
       | NONE => [])
   | parse_named _ _ = [];
 
-val jedit_actions =
+val isabelle_jedit_actions =
   (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
     XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
   | _ => []);
 
-val jedit_dockables =
+val isabelle_jedit_dockables =
   (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
     XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
   | _ => []);
 
-val all_actions = jedit_actions @ jedit_dockables;
+val jedit_actions =
+  Lazy.lazy (fn () =>
+    (case Isabelle_System.bash_output
+      "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
+      (txt, 0) =>
+        (case XML.parse txt of
+          XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
+        | _ => [])
+    | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
 
 in
 
-val is_action = member (op =) all_actions;
+fun is_action a =
+  member (op =) isabelle_jedit_actions a orelse
+  member (op =) isabelle_jedit_dockables a orelse
+  member (op =) (Lazy.force jedit_actions) a;
 
 end;