1 (* Title: Pure/PIDE/markup.ML
4 Isabelle-specific implementation of quasi-abstract markup elements.
9 val parse_int: string -> int
10 val print_int: int -> string
11 type T = string * Properties.T
13 val is_empty: T -> bool
14 val properties: Properties.T -> T -> T
16 val name: string -> T -> T
18 val bindingN: string val binding: T
19 val entityN: string val entity: string -> string -> T
20 val get_entity_kind: T -> string option
25 val end_offsetN: string
28 val position_properties': string list
29 val position_properties: string list
30 val positionN: string val position: T
31 val pathN: string val path: string -> T
33 val blockN: string val block: int -> T
35 val breakN: string val break: int -> T
36 val fbreakN: string val fbreak: T
37 val hiddenN: string val hidden: T
40 val type_nameN: string
42 val fixedN: string val fixed: string -> T
43 val dynamic_factN: string val dynamic_fact: string -> T
44 val tfreeN: string val tfree: T
45 val tvarN: string val tvar: T
46 val freeN: string val free: T
47 val skolemN: string val skolem: T
48 val boundN: string val bound: T
49 val varN: string val var: T
50 val numeralN: string val numeral: T
51 val literalN: string val literal: T
52 val delimiterN: string val delimiter: T
53 val inner_stringN: string val inner_string: T
54 val inner_commentN: string val inner_comment: T
55 val token_rangeN: string val token_range: T
56 val sortN: string val sort: T
57 val typN: string val typ: T
58 val termN: string val term: T
59 val propN: string val prop: T
60 val sortingN: string val sorting: T
61 val typingN: string val typing: T
62 val ML_keywordN: string val ML_keyword: T
63 val ML_delimiterN: string val ML_delimiter: T
64 val ML_tvarN: string val ML_tvar: T
65 val ML_numeralN: string val ML_numeral: T
66 val ML_charN: string val ML_char: T
67 val ML_stringN: string val ML_string: T
68 val ML_commentN: string val ML_comment: T
71 val ML_structN: string
72 val ML_typingN: string val ML_typing: T
73 val ML_sourceN: string val ML_source: T
74 val doc_sourceN: string val doc_source: T
75 val antiqN: string val antiq: T
76 val ML_antiquotationN: string
77 val document_antiquotationN: string
78 val document_antiquotation_optionN: string
79 val paragraphN: string val paragraph: T
80 val text_foldN: string val text_fold: T
81 val keywordN: string val keyword: T
82 val operatorN: string val operator: T
83 val commandN: string val command: T
84 val stringN: string val string: T
85 val altstringN: string val altstring: T
86 val verbatimN: string val verbatim: T
87 val commentN: string val comment: T
88 val controlN: string val control: T
89 val tokenN: string val token: Properties.T -> T
90 val keyword1N: string val keyword1: T
91 val keyword2N: string val keyword2: T
95 val timing_properties: Timing.timing -> Properties.T
96 val timingN: string val timing: Timing.timing -> T
98 val proof_stateN: string val proof_state: int -> T
99 val stateN: string val state: T
100 val goalN: string val goal: T
101 val subgoalN: string val subgoal: string -> T
103 val acceptedN: string val accepted: T
104 val forkedN: string val forked: T
105 val joinedN: string val joined: T
106 val runningN: string val running: T
107 val finishedN: string val finished: T
108 val failedN: string val failed: T
118 val protocolN: string
119 val legacyN: string val legacy: T
120 val promptN: string val prompt: T
121 val reportN: string val report: T
122 val no_reportN: string val no_report: T
123 val badN: string val bad: T
124 val intensifyN: string val intensify: T
126 val graphviewN: string
127 val sendbackN: string
129 val padding_line: Properties.entry
130 val dialogN: string val dialog: serial -> string -> T
131 val functionN: string
132 val assign_execs: Properties.T
133 val removed_versions: Properties.T
134 val invoke_scala: string -> string -> Properties.T
135 val cancel_scala: string -> Properties.T
136 val ML_statistics: Properties.entry
137 val task_statistics: Properties.entry
138 val command_timing: Properties.entry
139 val loading_theory: string -> Properties.T
140 val dest_loading_theory: Properties.T -> string option
141 val no_output: Output.output * Output.output
142 val default_output: T -> Output.output * Output.output
143 val add_mode: string -> (T -> Output.output * Output.output) -> unit
144 val output: T -> Output.output * Output.output
145 val enclose: T -> Output.output -> Output.output
146 val markup: T -> string -> string
147 val markup_only: T -> string
150 structure Markup: MARKUP =
153 (** markup elements **)
158 let val i = Int.fromString s in
159 if is_none i orelse String.isPrefix "~" s
160 then raise Fail ("Bad integer: " ^ quote s)
164 val print_int = signed_string_of_int;
169 type T = string * Properties.T;
171 val empty = ("", []);
173 fun is_empty ("", _) = true
174 | is_empty _ = false;
177 fun properties more_props ((elem, props): T) =
178 (elem, fold_rev Properties.put more_props props);
180 fun markup_elem elem = (elem, (elem, []): T);
181 fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
182 fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
185 (* misc properties *)
188 fun name a = properties [(nameN, a)];
193 (* formal entities *)
195 val (bindingN, binding) = markup_elem "binding";
197 val entityN = "entity";
198 fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
200 fun get_entity_kind (name, props) =
201 if name = entityN then AList.lookup (op =) props kindN
211 val offsetN = "offset";
212 val end_offsetN = "end_offset";
216 val position_properties' = [fileN, idN];
217 val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
219 val (positionN, position) = markup_elem "position";
224 val (pathN, path) = markup_string "path" nameN;
227 (* pretty printing *)
229 val indentN = "indent";
230 val (blockN, block) = markup_int "block" indentN;
232 val widthN = "width";
233 val (breakN, break) = markup_int "break" widthN;
235 val (fbreakN, fbreak) = markup_elem "fbreak";
240 val (hiddenN, hidden) = markup_elem "hidden";
243 (* logical entities *)
245 val theoryN = "theory";
246 val classN = "class";
247 val type_nameN = "type_name";
248 val constantN = "constant";
250 val (fixedN, fixed) = markup_string "fixed" nameN;
251 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
256 val (tfreeN, tfree) = markup_elem "tfree";
257 val (tvarN, tvar) = markup_elem "tvar";
258 val (freeN, free) = markup_elem "free";
259 val (skolemN, skolem) = markup_elem "skolem";
260 val (boundN, bound) = markup_elem "bound";
261 val (varN, var) = markup_elem "var";
262 val (numeralN, numeral) = markup_elem "numeral";
263 val (literalN, literal) = markup_elem "literal";
264 val (delimiterN, delimiter) = markup_elem "delimiter";
265 val (inner_stringN, inner_string) = markup_elem "inner_string";
266 val (inner_commentN, inner_comment) = markup_elem "inner_comment";
268 val (token_rangeN, token_range) = markup_elem "token_range";
270 val (sortN, sort) = markup_elem "sort";
271 val (typN, typ) = markup_elem "typ";
272 val (termN, term) = markup_elem "term";
273 val (propN, prop) = markup_elem "prop";
275 val (sortingN, sorting) = markup_elem "sorting";
276 val (typingN, typing) = markup_elem "typing";
281 val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
282 val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
283 val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
284 val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
285 val (ML_charN, ML_char) = markup_elem "ML_char";
286 val (ML_stringN, ML_string) = markup_elem "ML_string";
287 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
289 val ML_defN = "ML_def";
290 val ML_openN = "ML_open";
291 val ML_structN = "ML_struct";
292 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
295 (* embedded source text *)
297 val (ML_sourceN, ML_source) = markup_elem "ML_source";
298 val (doc_sourceN, doc_source) = markup_elem "doc_source";
300 val (antiqN, antiq) = markup_elem "antiq";
301 val ML_antiquotationN = "ML_antiquotation";
302 val document_antiquotationN = "document_antiquotation";
303 val document_antiquotation_optionN = "document_antiquotation_option";
308 val (paragraphN, paragraph) = markup_elem "paragraph";
309 val (text_foldN, text_fold) = markup_elem "text_fold";
314 val (keywordN, keyword) = markup_elem "keyword";
315 val (operatorN, operator) = markup_elem "operator";
316 val (commandN, command) = markup_elem "command";
317 val (stringN, string) = markup_elem "string";
318 val (altstringN, altstring) = markup_elem "altstring";
319 val (verbatimN, verbatim) = markup_elem "verbatim";
320 val (commentN, comment) = markup_elem "comment";
321 val (controlN, control) = markup_elem "control";
323 val tokenN = "token";
324 fun token props = (tokenN, props);
326 val (keyword1N, keyword1) = markup_elem "keyword1";
327 val (keyword2N, keyword2) = markup_elem "keyword2";
332 val elapsedN = "elapsed";
336 fun timing_properties {elapsed, cpu, gc} =
337 [(elapsedN, Time.toString elapsed),
338 (cpuN, Time.toString cpu),
339 (gcN, Time.toString gc)];
341 val timingN = "timing";
342 fun timing t = (timingN, timing_properties t);
347 val subgoalsN = "subgoals";
348 val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
350 val (stateN, state) = markup_elem "state";
351 val (goalN, goal) = markup_elem "goal";
352 val (subgoalN, subgoal) = markup_string "subgoal" nameN;
359 val (acceptedN, accepted) = markup_elem "accepted";
360 val (forkedN, forked) = markup_elem "forked";
361 val (joinedN, joined) = markup_elem "joined";
362 val (runningN, running) = markup_elem "running";
363 val (finishedN, finished) = markup_elem "finished";
364 val (failedN, failed) = markup_elem "failed";
369 val serialN = "serial";
370 val exec_idN = "exec_id";
373 val statusN = "status";
374 val resultN = "result";
375 val writelnN = "writeln";
376 val tracingN = "tracing";
377 val warningN = "warning";
378 val errorN = "error";
379 val protocolN = "protocol";
381 val (legacyN, legacy) = markup_elem "legacy";
382 val (promptN, prompt) = markup_elem "prompt";
384 val (reportN, report) = markup_elem "report";
385 val (no_reportN, no_report) = markup_elem "no_report";
387 val (badN, bad) = markup_elem "bad";
389 val (intensifyN, intensify) = markup_elem "intensify";
394 val browserN = "browser"
395 val graphviewN = "graphview";
397 val sendbackN = "sendback";
398 val paddingN = "padding";
399 val padding_line = (paddingN, lineN);
401 val dialogN = "dialog";
402 fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
405 (* protocol message functions *)
407 val functionN = "function"
409 val assign_execs = [(functionN, "assign_execs")];
410 val removed_versions = [(functionN, "removed_versions")];
412 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
413 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
415 val ML_statistics = (functionN, "ML_statistics");
417 val task_statistics = (functionN, "task_statistics");
419 val command_timing = (functionN, "command_timing");
421 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
423 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
424 | dest_loading_theory _ = NONE;
428 (** print mode operations **)
430 val no_output = ("", "");
431 fun default_output (_: T) = no_output;
434 val default = {output = default_output};
435 val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
437 fun add_mode name output =
438 Synchronized.change modes (fn tab =>
439 (if not (Symtab.defined tab name) then ()
440 else warning ("Redefining markup mode " ^ quote name);
441 Symtab.update (name, {output = output}) tab));
444 (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
447 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
449 val enclose = output #-> Library.enclose;
452 let val (bg, en) = output m
453 in Library.enclose (Output.escape bg) (Output.escape en) end;
455 fun markup_only m = markup m "";