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