author | wenzelm |
Fri, 20 Apr 2012 23:16:46 +0200 | |
changeset 47633 | e5c5e73f3e30 |
parent 46894 | e2ad717ec889 |
child 50201 | c26369c9eda6 |
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 |
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
18 |
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
|
19 |
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
|
20 |
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
|
21 |
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
|
22 |
val enclose: T -> Output.output -> Output.output |
25552 | 23 |
val markup: T -> string -> string |
43665 | 24 |
val markup_only: T -> string |
23623 | 25 |
end; |
26 |
||
27 |
structure Markup: MARKUP = |
|
28 |
struct |
|
29 |
||
30221 | 30 |
(** markup elements **) |
31 |
||
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
32 |
(* integers *) |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
33 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
34 |
fun parse_int s = |
43797
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
35 |
let val i = Int.fromString s in |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
36 |
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
|
37 |
then raise Fail ("Bad integer: " ^ quote s) |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
38 |
else the i |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
39 |
end; |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
40 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
41 |
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
|
42 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
43 |
|
23658 | 44 |
(* basic markup *) |
23623 | 45 |
|
28017 | 46 |
type T = string * Properties.T; |
23637 | 47 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
48 |
val empty = ("", []); |
23637 | 49 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
50 |
fun is_empty ("", _) = true |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
51 |
| is_empty _ = false; |
27883 | 52 |
|
23794 | 53 |
|
23671 | 54 |
fun properties more_props ((elem, props): T) = |
28017 | 55 |
(elem, fold_rev Properties.put more_props props); |
23671 | 56 |
|
26977 | 57 |
|
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
58 |
(* misc properties *) |
26977 | 59 |
|
23658 | 60 |
val nameN = "name"; |
27818 | 61 |
fun name a = properties [(nameN, a)]; |
62 |
||
23658 | 63 |
val kindN = "kind"; |
23671 | 64 |
|
23658 | 65 |
|
27969 | 66 |
|
30221 | 67 |
(** print mode operations **) |
23704 | 68 |
|
29325 | 69 |
val no_output = ("", ""); |
70 |
fun default_output (_: T) = no_output; |
|
23704 | 71 |
|
72 |
local |
|
73 |
val default = {output = default_output}; |
|
43684 | 74 |
val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]); |
23704 | 75 |
in |
43684 | 76 |
fun add_mode name output = |
46894
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45674
diff
changeset
|
77 |
Synchronized.change modes (fn tab => |
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45674
diff
changeset
|
78 |
(if not (Symtab.defined tab name) then () |
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45674
diff
changeset
|
79 |
else warning ("Redefining markup mode " ^ quote name); |
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45674
diff
changeset
|
80 |
Symtab.update (name, {output = output}) tab)); |
23704 | 81 |
fun get_mode () = |
43684 | 82 |
the_default default |
83 |
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); |
|
23623 | 84 |
end; |
23704 | 85 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
86 |
fun output m = if is_empty m then no_output else #output (get_mode ()) m; |
23704 | 87 |
|
23719 | 88 |
val enclose = output #-> Library.enclose; |
89 |
||
25552 | 90 |
fun markup m = |
91 |
let val (bg, en) = output m |
|
92 |
in Library.enclose (Output.escape bg) (Output.escape en) end; |
|
93 |
||
43665 | 94 |
fun markup_only m = markup m ""; |
95 |
||
23704 | 96 |
end; |