author | wenzelm |
Tue, 29 Nov 2011 19:49:36 +0100 | |
changeset 45670 | b84170538043 |
parent 45666 | src/Pure/General/markup.ML@d83797ef0d2d |
child 45674 | eb65c9d17e2f |
permissions | -rw-r--r-- |
45670 | 1 |
(* Title: Pure/PIDE/markup.ML |
23623 | 2 |
Author: Makarius |
3 |
||
45666 | 4 |
Generic markup elements. |
23623 | 5 |
*) |
6 |
||
7 |
signature MARKUP = |
|
8 |
sig |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
9 |
val parse_int: string -> int |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
10 |
val print_int: int -> string |
28017 | 11 |
type T = string * Properties.T |
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
12 |
val empty: T |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
13 |
val is_empty: T -> bool |
38229 | 14 |
val properties: Properties.T -> T -> T |
23623 | 15 |
val nameN: string |
27818 | 16 |
val name: string -> T -> T |
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38871
diff
changeset
|
17 |
val kindN: string |
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
18 |
val elapsedN: string |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
19 |
val cpuN: string |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
20 |
val gcN: string |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41484
diff
changeset
|
21 |
val timingN: string val timing: Timing.timing -> T |
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
22 |
val no_output: Output.output * Output.output |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
23 |
val default_output: T -> Output.output * Output.output |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
24 |
val add_mode: string -> (T -> Output.output * Output.output) -> unit |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
25 |
val output: T -> Output.output * Output.output |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
26 |
val enclose: T -> Output.output -> Output.output |
25552 | 27 |
val markup: T -> string -> string |
43665 | 28 |
val markup_only: T -> string |
23623 | 29 |
end; |
30 |
||
31 |
structure Markup: MARKUP = |
|
32 |
struct |
|
33 |
||
30221 | 34 |
(** markup elements **) |
35 |
||
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
36 |
(* integers *) |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
37 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
38 |
fun parse_int s = |
43797
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
39 |
let val i = Int.fromString s in |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
40 |
if is_none i orelse String.isPrefix "~" s |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
41 |
then raise Fail ("Bad integer: " ^ quote s) |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
42 |
else the i |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
43 |
end; |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
44 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
45 |
val print_int = signed_string_of_int; |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
46 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
47 |
|
23658 | 48 |
(* basic markup *) |
23623 | 49 |
|
28017 | 50 |
type T = string * Properties.T; |
23637 | 51 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
52 |
val empty = ("", []); |
23637 | 53 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
54 |
fun is_empty ("", _) = true |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
55 |
| is_empty _ = false; |
27883 | 56 |
|
23794 | 57 |
|
23671 | 58 |
fun properties more_props ((elem, props): T) = |
28017 | 59 |
(elem, fold_rev Properties.put more_props props); |
23671 | 60 |
|
26977 | 61 |
|
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
62 |
(* misc properties *) |
26977 | 63 |
|
23658 | 64 |
val nameN = "name"; |
27818 | 65 |
fun name a = properties [(nameN, a)]; |
66 |
||
23658 | 67 |
val kindN = "kind"; |
23671 | 68 |
|
23658 | 69 |
|
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
70 |
(* timing *) |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
71 |
|
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
72 |
val timingN = "timing"; |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
73 |
val elapsedN = "elapsed"; |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
74 |
val cpuN = "cpu"; |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
75 |
val gcN = "gc"; |
23637 | 76 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41484
diff
changeset
|
77 |
fun timing {elapsed, cpu, gc} = |
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
78 |
(timingN, |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
79 |
[(elapsedN, Time.toString elapsed), |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
80 |
(cpuN, Time.toString cpu), |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
81 |
(gcN, Time.toString gc)]); |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
82 |
|
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset
|
83 |
|
27969 | 84 |
|
30221 | 85 |
(** print mode operations **) |
23704 | 86 |
|
29325 | 87 |
val no_output = ("", ""); |
88 |
fun default_output (_: T) = no_output; |
|
23704 | 89 |
|
90 |
local |
|
91 |
val default = {output = default_output}; |
|
43684 | 92 |
val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]); |
23704 | 93 |
in |
43684 | 94 |
fun add_mode name output = |
95 |
Synchronized.change modes (Symtab.update_new (name, {output = output})); |
|
23704 | 96 |
fun get_mode () = |
43684 | 97 |
the_default default |
98 |
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); |
|
23623 | 99 |
end; |
23704 | 100 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
101 |
fun output m = if is_empty m then no_output else #output (get_mode ()) m; |
23704 | 102 |
|
23719 | 103 |
val enclose = output #-> Library.enclose; |
104 |
||
25552 | 105 |
fun markup m = |
106 |
let val (bg, en) = output m |
|
107 |
in Library.enclose (Output.escape bg) (Output.escape en) end; |
|
108 |
||
43665 | 109 |
fun markup_only m = markup m ""; |
110 |
||
23704 | 111 |
end; |