--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/jedit.ML Tue Nov 10 20:10:17 2015 +0100
@@ -0,0 +1,56 @@
+(* Title: Pure/Tools/jedit.ML
+ Author: Makarius
+
+jEdit support.
+*)
+
+signature JEDIT =
+sig
+ val is_action: string -> bool
+end;
+
+structure JEdit: JEDIT =
+struct
+
+(* jEdit actions *)
+
+local
+
+fun parse_named a (XML.Elem ((b, props), _)) =
+ (case Properties.get props "NAME" of
+ SOME name => if a = b then [name] else []
+ | NONE => [])
+ | parse_named _ _ = [];
+
+val isabelle_jedit_actions =
+ Lazy.lazy (fn () =>
+ (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
+ XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
+ | _ => []));
+
+val isabelle_jedit_dockables =
+ Lazy.lazy (fn () =>
+ (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
+ XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
+ | _ => []));
+
+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
+
+fun is_action a =
+ member (op =) (Lazy.force isabelle_jedit_actions) a orelse
+ member (op =) (Lazy.force isabelle_jedit_dockables) a orelse
+ member (op =) (Lazy.force jedit_actions) a;
+
+end;
+
+end;