1 (* Title: Pure/Tools/jedit.ML |
1 (* Title: Pure/Tools/jedit.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 jEdit support. |
4 Support for Isabelle/jEdit. |
5 *) |
5 *) |
6 |
6 |
7 signature JEDIT = |
7 signature JEDIT = |
8 sig |
8 sig |
|
9 val get_actions: unit -> string list |
9 val check_action: string * Position.T -> string |
10 val check_action: string * Position.T -> string |
10 end; |
11 end; |
11 |
12 |
12 structure JEdit: JEDIT = |
13 structure JEdit: JEDIT = |
13 struct |
14 struct |
14 |
15 |
15 (* jEdit actions *) |
16 (* parse XML *) |
16 |
|
17 local |
|
18 |
17 |
19 fun parse_named a (XML.Elem ((b, props), _)) = |
18 fun parse_named a (XML.Elem ((b, props), _)) = |
20 (case Properties.get props "NAME" of |
19 (case Properties.get props "NAME" of |
21 SOME name => if a = b then [name] else [] |
20 SOME name => if a = b then [name] else [] |
22 | NONE => []) |
21 | NONE => []) |
23 | parse_named _ _ = []; |
22 | parse_named _ _ = []; |
24 |
23 |
25 val isabelle_jedit_actions = |
24 fun parse_actions (XML.Elem (("ACTIONS", _), body)) = maps (parse_named "ACTION") body |
|
25 | parse_actions _ = []; |
|
26 |
|
27 fun parse_dockables (XML.Elem (("DOCKABLES", _), body)) = |
|
28 maps (parse_named "DOCKABLE") body |
|
29 |> maps (fn a => [a, a ^ "-toggle", a ^ "-float"]) |
|
30 | parse_dockables _ = []; |
|
31 |
|
32 |
|
33 (* XML resources *) |
|
34 |
|
35 val xml_file = XML.parse o File.read; |
|
36 |
|
37 fun xml_resource name = |
|
38 let val script = "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name in |
|
39 (case Isabelle_System.bash_output script of |
|
40 (txt, 0) => XML.parse txt |
|
41 | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)) |
|
42 end; |
|
43 |
|
44 |
|
45 (* actions *) |
|
46 |
|
47 val lazy_actions = |
26 Lazy.lazy (fn () => |
48 Lazy.lazy (fn () => |
27 (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/actions.xml\<close>) of |
49 (parse_actions (xml_file \<^file>\<open>~~/src/Tools/jEdit/src/actions.xml\<close>) @ |
28 XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body |
50 parse_dockables (xml_file \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) @ |
29 | _ => [])); |
51 parse_actions (xml_resource "org/gjt/sp/jedit/actions.xml")) |
|
52 |> sort_strings); |
30 |
53 |
31 val isabelle_jedit_dockables = |
54 fun get_actions () = Lazy.force lazy_actions; |
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 |
55 |
56 fun check_action (name, pos) = |
56 fun check_action (name, pos) = |
57 if member (op =) (Lazy.force all_actions) name then |
57 if member (op =) (get_actions ()) name then |
58 let |
58 let |
59 val ((bg1, bg2), en) = |
59 val ((bg1, bg2), en) = |
60 YXML.output_markup_elem |
60 YXML.output_markup_elem |
61 (Active.make_markup Markup.jedit_actionN {implicit = false, properties = []}); |
61 (Active.make_markup Markup.jedit_actionN {implicit = false, properties = []}); |
62 val msg = "Invoke " ^ bg1 ^ name ^ bg2 ^ name ^ en ^ " jEdit action"; |
62 val msg = "Invoke " ^ bg1 ^ name ^ bg2 ^ name ^ en ^ " jEdit action"; |
64 else |
64 else |
65 let |
65 let |
66 val completion_report = |
66 val completion_report = |
67 Completion.make_report (name, pos) |
67 Completion.make_report (name, pos) |
68 (fn completed => |
68 (fn completed => |
69 Lazy.force all_actions |
69 get_actions () |
70 |> filter completed |
70 |> filter completed |
71 |> sort_strings |
71 |> sort_strings |
72 |> map (fn a => (a, ("action", a)))); |
72 |> map (fn a => (a, ("action", a)))); |
73 in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ completion_report) end |
73 in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ completion_report) end; |
74 |
74 |
75 val _ = |
75 val _ = |
76 Theory.setup |
76 Theory.setup |
77 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position) |
77 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position) |
78 (fn ctxt => fn (name, pos) => |
78 (fn ctxt => fn (name, pos) => |