author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 74563 | 042041c0ebeb |
child 76552 | 13fde66c7cf6 |
permissions | -rw-r--r-- |
61617 | 1 |
(* Title: Pure/Tools/jedit.ML |
2 |
Author: Makarius |
|
3 |
||
71513 | 4 |
Support for Isabelle/jEdit. |
61617 | 5 |
*) |
6 |
||
7 |
signature JEDIT = |
|
8 |
sig |
|
71513 | 9 |
val get_actions: unit -> string list |
61620 | 10 |
val check_action: string * Position.T -> string |
61617 | 11 |
end; |
12 |
||
13 |
structure JEdit: JEDIT = |
|
14 |
struct |
|
15 |
||
71513 | 16 |
(* parse XML *) |
61617 | 17 |
|
18 |
fun parse_named a (XML.Elem ((b, props), _)) = |
|
19 |
(case Properties.get props "NAME" of |
|
20 |
SOME name => if a = b then [name] else [] |
|
21 |
| NONE => []) |
|
22 |
| parse_named _ _ = []; |
|
23 |
||
71513 | 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 *) |
|
61617 | 34 |
|
71513 | 35 |
val xml_file = XML.parse o File.read; |
61617 | 36 |
|
71513 | 37 |
fun xml_resource name = |
73282 | 38 |
let |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
39 |
val res = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
40 |
Isabelle_System.bash_process (Bash.script ("unzip -p \"$JEDIT_JAR\" " ^ Bash.string name)); |
73282 | 41 |
val rc = Process_Result.rc res; |
42 |
in |
|
43 |
res |> Process_Result.check |> Process_Result.out |> XML.parse |
|
44 |
handle ERROR _ => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc) |
|
71513 | 45 |
end; |
46 |
||
47 |
||
48 |
(* actions *) |
|
49 |
||
50 |
val lazy_actions = |
|
61617 | 51 |
Lazy.lazy (fn () => |
73987
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73761
diff
changeset
|
52 |
(parse_actions (xml_file \<^file>\<open>~~/src/Tools/jEdit/jedit_main/actions.xml\<close>) @ |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73761
diff
changeset
|
53 |
parse_dockables (xml_file \<^file>\<open>~~/src/Tools/jEdit/jedit_main/dockables.xml\<close>) @ |
71514
61882acca79b
include actions for jEdit dockables, e.g. "vfs.browser";
wenzelm
parents:
71513
diff
changeset
|
54 |
parse_actions (xml_resource "org/gjt/sp/jedit/actions.xml") @ |
61882acca79b
include actions for jEdit dockables, e.g. "vfs.browser";
wenzelm
parents:
71513
diff
changeset
|
55 |
parse_dockables (xml_resource "org/gjt/sp/jedit/dockables.xml")) |
71513 | 56 |
|> sort_strings); |
61617 | 57 |
|
71513 | 58 |
fun get_actions () = Lazy.force lazy_actions; |
61620 | 59 |
|
61621
70b8085f51b4
more thorough check_action, including completion;
wenzelm
parents:
61620
diff
changeset
|
60 |
fun check_action (name, pos) = |
71513 | 61 |
if member (op =) (get_actions ()) name then |
63681 | 62 |
let |
63 |
val ((bg1, bg2), en) = |
|
64 |
YXML.output_markup_elem |
|
65 |
(Active.make_markup Markup.jedit_actionN {implicit = false, properties = []}); |
|
66 |
val msg = "Invoke " ^ bg1 ^ name ^ bg2 ^ name ^ en ^ " jEdit action"; |
|
67 |
in writeln (msg ^ Position.here pos); name end |
|
61621
70b8085f51b4
more thorough check_action, including completion;
wenzelm
parents:
61620
diff
changeset
|
68 |
else |
70b8085f51b4
more thorough check_action, including completion;
wenzelm
parents:
61620
diff
changeset
|
69 |
let |
69289 | 70 |
val completion_report = |
71 |
Completion.make_report (name, pos) |
|
61621
70b8085f51b4
more thorough check_action, including completion;
wenzelm
parents:
61620
diff
changeset
|
72 |
(fn completed => |
71513 | 73 |
get_actions () |
61621
70b8085f51b4
more thorough check_action, including completion;
wenzelm
parents:
61620
diff
changeset
|
74 |
|> filter completed |
70b8085f51b4
more thorough check_action, including completion;
wenzelm
parents:
61620
diff
changeset
|
75 |
|> sort_strings |
70b8085f51b4
more thorough check_action, including completion;
wenzelm
parents:
61620
diff
changeset
|
76 |
|> map (fn a => (a, ("action", a)))); |
71513 | 77 |
in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ completion_report) end; |
61620 | 78 |
|
63681 | 79 |
val _ = |
80 |
Theory.setup |
|
74563 | 81 |
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close> |
82 |
(Scan.lift Parse.embedded_position) |
|
67463 | 83 |
(fn ctxt => fn (name, pos) => |
84 |
let |
|
85 |
val _ = |
|
86 |
if Context_Position.is_reported ctxt pos |
|
87 |
then ignore (check_action (name, pos)) |
|
88 |
else (); |
|
89 |
in name end)); |
|
63681 | 90 |
|
61617 | 91 |
end; |