src/Pure/Tools/jedit.ML
author wenzelm
Tue Nov 10 20:10:17 2015 +0100 (2015-11-10)
changeset 61617 cd7549cd5fe7
child 61620 01db1bed4487
permissions -rw-r--r--
clarified modules;
     1 (*  Title:      Pure/Tools/jedit.ML
     2     Author:     Makarius
     3 
     4 jEdit support.
     5 *)
     6 
     7 signature JEDIT =
     8 sig
     9   val is_action: string -> bool
    10 end;
    11 
    12 structure JEdit: JEDIT =
    13 struct
    14 
    15 (* jEdit actions *)
    16 
    17 local
    18 
    19 fun parse_named a (XML.Elem ((b, props), _)) =
    20       (case Properties.get props "NAME" of
    21         SOME name => if a = b then [name] else []
    22       | NONE => [])
    23   | parse_named _ _ = [];
    24 
    25 val isabelle_jedit_actions =
    26   Lazy.lazy (fn () =>
    27     (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
    28       XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
    29     | _ => []));
    30 
    31 val isabelle_jedit_dockables =
    32   Lazy.lazy (fn () =>
    33     (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
    34       XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
    35     | _ => []));
    36 
    37 val jedit_actions =
    38   Lazy.lazy (fn () =>
    39     (case Isabelle_System.bash_output
    40       "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
    41       (txt, 0) =>
    42         (case XML.parse txt of
    43           XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
    44         | _ => [])
    45     | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
    46 
    47 in
    48 
    49 fun is_action a =
    50   member (op =) (Lazy.force isabelle_jedit_actions) a orelse
    51   member (op =) (Lazy.force isabelle_jedit_dockables) a orelse
    52   member (op =) (Lazy.force jedit_actions) a;
    53 
    54 end;
    55 
    56 end;