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