src/Doc/antiquote_setup.ML
changeset 57334 54c6b73774d2
parent 56467 8d7d6f17c6a7
child 57477 c3b5cb53ea79
equal deleted inserted replaced
57333:d58b7f7d81db 57334:54c6b73774d2
   164       (case Properties.get props "NAME" of
   164       (case Properties.get props "NAME" of
   165         SOME name => if a = b then [name] else []
   165         SOME name => if a = b then [name] else []
   166       | NONE => [])
   166       | NONE => [])
   167   | parse_named _ _ = [];
   167   | parse_named _ _ = [];
   168 
   168 
   169 val jedit_actions =
   169 val isabelle_jedit_actions =
   170   (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
   170   (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
   171     XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
   171     XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
   172   | _ => []);
   172   | _ => []);
   173 
   173 
   174 val jedit_dockables =
   174 val isabelle_jedit_dockables =
   175   (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
   175   (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
   176     XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
   176     XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
   177   | _ => []);
   177   | _ => []);
   178 
   178 
   179 val all_actions = jedit_actions @ jedit_dockables;
   179 val jedit_actions =
       
   180   Lazy.lazy (fn () =>
       
   181     (case Isabelle_System.bash_output
       
   182       "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
       
   183       (txt, 0) =>
       
   184         (case XML.parse txt of
       
   185           XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
       
   186         | _ => [])
       
   187     | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
   180 
   188 
   181 in
   189 in
   182 
   190 
   183 val is_action = member (op =) all_actions;
   191 fun is_action a =
       
   192   member (op =) isabelle_jedit_actions a orelse
       
   193   member (op =) isabelle_jedit_dockables a orelse
       
   194   member (op =) (Lazy.force jedit_actions) a;
   184 
   195 
   185 end;
   196 end;
   186 
   197 
   187 
   198 
   188 (* Isabelle/Isar entities (with index) *)
   199 (* Isabelle/Isar entities (with index) *)