1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/jedit.ML	Tue Nov 10 20:10:17 2015 +0100
     1.3 @@ -0,0 +1,56 @@
     1.4 +(*  Title:      Pure/Tools/jedit.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +jEdit support.
     1.8 +*)
     1.9 +
    1.10 +signature JEDIT =
    1.11 +sig
    1.12 +  val is_action: string -> bool
    1.13 +end;
    1.14 +
    1.15 +structure JEdit: JEDIT =
    1.16 +struct
    1.17 +
    1.18 +(* jEdit actions *)
    1.19 +
    1.20 +local
    1.21 +
    1.22 +fun parse_named a (XML.Elem ((b, props), _)) =
    1.23 +      (case Properties.get props "NAME" of
    1.24 +        SOME name => if a = b then [name] else []
    1.25 +      | NONE => [])
    1.26 +  | parse_named _ _ = [];
    1.27 +
    1.28 +val isabelle_jedit_actions =
    1.29 +  Lazy.lazy (fn () =>
    1.30 +    (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
    1.31 +      XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
    1.32 +    | _ => []));
    1.33 +
    1.34 +val isabelle_jedit_dockables =
    1.35 +  Lazy.lazy (fn () =>
    1.36 +    (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
    1.37 +      XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
    1.38 +    | _ => []));
    1.39 +
    1.40 +val jedit_actions =
    1.41 +  Lazy.lazy (fn () =>
    1.42 +    (case Isabelle_System.bash_output
    1.43 +      "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
    1.44 +      (txt, 0) =>
    1.45 +        (case XML.parse txt of
    1.46 +          XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
    1.47 +        | _ => [])
    1.48 +    | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
    1.49 +
    1.50 +in
    1.51 +
    1.52 +fun is_action a =
    1.53 +  member (op =) (Lazy.force isabelle_jedit_actions) a orelse
    1.54 +  member (op =) (Lazy.force isabelle_jedit_dockables) a orelse
    1.55 +  member (op =) (Lazy.force jedit_actions) a;
    1.56 +
    1.57 +end;
    1.58 +
    1.59 +end;