src/Pure/Tools/jedit.ML
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 66670 e5188cb1c3d8
child 67147 dea94b1aabc3
permissions -rw-r--r--
tuned signature;
     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 \<^file>\<open>~~/src/Tools/jEdit/src/actions.xml\<close>) 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 \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) of
    34       XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
    35     | _ => [])
    36     |> maps (fn a => [a, a ^ "-toggle", a ^ "-float"]));
    37 
    38 val jedit_actions =
    39   Lazy.lazy (fn () =>
    40     (case Isabelle_System.bash_output
    41       "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
    42       (txt, 0) =>
    43         (case XML.parse txt of
    44           XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
    45         | _ => [])
    46     | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
    47 
    48 val all_actions =
    49   Lazy.lazy (fn () =>
    50     Lazy.force isabelle_jedit_actions @
    51     Lazy.force isabelle_jedit_dockables @
    52     Lazy.force jedit_actions);
    53 
    54 in
    55 
    56 fun check_action (name, pos) =
    57   if member (op =) (Lazy.force all_actions) name then
    58     let
    59       val ((bg1, bg2), en) =
    60         YXML.output_markup_elem
    61           (Active.make_markup Markup.jedit_actionN {implicit = false, properties = []});
    62       val msg = "Invoke " ^ bg1 ^ name ^ bg2 ^ name ^ en ^ " jEdit action";
    63     in writeln (msg ^ Position.here pos); name end
    64   else
    65     let
    66       val completion =
    67         Completion.make (name, pos)
    68           (fn completed =>
    69             Lazy.force all_actions
    70             |> filter completed
    71             |> sort_strings
    72             |> map (fn a => (a, ("action", a))));
    73       val report = Markup.markup_report (Completion.reported_text completion);
    74     in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ report) end
    75 
    76 val _ =
    77   Theory.setup
    78     (Thy_Output.antiquotation @{binding action} (Scan.lift (Parse.position Parse.embedded))
    79       (fn {context = ctxt, ...} => fn (name, pos) =>
    80        (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
    81         Thy_Output.verbatim_text ctxt name)));
    82 
    83 end;
    84 
    85 end;