src/Pure/Tools/jedit.ML
author wenzelm
Tue Nov 10 22:20:46 2015 +0100 (2015-11-10)
changeset 61621 70b8085f51b4
parent 61620 01db1bed4487
child 63669 256fc20716f2
permissions -rw-r--r--
more thorough check_action, including completion;
     1 (*  Title:      Pure/Tools/jedit.ML
     2     Author:     Makarius
     3 
     4 jEdit support.
     5 *)
     6 
     7 signature JEDIT =
     8 sig
     9   val check_action: string * Position.T -> string
    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 val all_actions =
    48   Lazy.lazy (fn () =>
    49     Lazy.force isabelle_jedit_actions @
    50     Lazy.force isabelle_jedit_dockables @
    51     Lazy.force jedit_actions);
    52 
    53 in
    54 
    55 fun check_action (name, pos) =
    56   if member (op =) (Lazy.force all_actions) name then name
    57   else
    58     let
    59       val completion =
    60         Completion.make (name, pos)
    61           (fn completed =>
    62             Lazy.force all_actions
    63             |> filter completed
    64             |> sort_strings
    65             |> map (fn a => (a, ("action", a))));
    66       val report = Markup.markup_report (Completion.reported_text completion);
    67     in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ report) end
    68 
    69 end;
    70 
    71 end;