author | blanchet |
Wed, 30 Jul 2014 23:52:56 +0200 | |
changeset 57720 | 9df2757f5bec |
parent 56467 | 8d7d6f17c6a7 |
child 59812 | 675d0c692c41 |
permissions | -rw-r--r-- |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/System/options.ML |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
3 |
|
51945 | 4 |
System options with external string representation. |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
5 |
*) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
6 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
7 |
signature OPTIONS = |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
8 |
sig |
51943 | 9 |
val boolT: string |
10 |
val intT: string |
|
11 |
val realT: string |
|
12 |
val stringT: string |
|
13 |
val unknownT: string |
|
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
14 |
type T |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
15 |
val empty: T |
56467 | 16 |
val markup: T -> string * Position.T -> Markup.T |
51942 | 17 |
val typ: T -> string -> string |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
18 |
val bool: T -> string -> bool |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
19 |
val int: T -> string -> int |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
20 |
val real: T -> string -> real |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
21 |
val string: T -> string -> string |
51943 | 22 |
val put_bool: string -> bool -> T -> T |
23 |
val put_int: string -> int -> T -> T |
|
24 |
val put_real: string -> real -> T -> T |
|
25 |
val put_string: string -> string -> T -> T |
|
56465 | 26 |
val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T |
51943 | 27 |
val update: string -> string -> T -> T |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
28 |
val decode: XML.body -> T |
48698
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
29 |
val default: unit -> T |
56467 | 30 |
val default_markup: string * Position.T -> Markup.T |
51946 | 31 |
val default_typ: string -> string |
51942 | 32 |
val default_bool: string -> bool |
33 |
val default_int: string -> int |
|
34 |
val default_real: string -> real |
|
35 |
val default_string: string -> string |
|
51943 | 36 |
val default_put_bool: string -> bool -> unit |
37 |
val default_put_int: string -> int -> unit |
|
38 |
val default_put_real: string -> real -> unit |
|
39 |
val default_put_string: string -> string -> unit |
|
40 |
val get_default: string -> string |
|
41 |
val put_default: string -> string -> unit |
|
48698
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
42 |
val set_default: T -> unit |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
43 |
val reset_default: unit -> unit |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
44 |
val load_default: unit -> unit |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
45 |
end; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
46 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
47 |
structure Options: OPTIONS = |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
48 |
struct |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
49 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
50 |
(* representation *) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
51 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
52 |
val boolT = "bool"; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
53 |
val intT = "int"; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
54 |
val realT = "real"; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
55 |
val stringT = "string"; |
51943 | 56 |
val unknownT = "unknown"; |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
57 |
|
56465 | 58 |
datatype T = Options of {pos: Position.T, typ: string, value: string} Symtab.table; |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
59 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
60 |
val empty = Options Symtab.empty; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
61 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
62 |
|
51943 | 63 |
(* check *) |
51942 | 64 |
|
51943 | 65 |
fun check_name (Options tab) name = |
66 |
let val opt = Symtab.lookup tab name in |
|
67 |
if is_some opt andalso #typ (the opt) <> unknownT then the opt |
|
51978 | 68 |
else error ("Unknown system option " ^ quote name) |
51943 | 69 |
end; |
70 |
||
71 |
fun check_type options name typ = |
|
72 |
let val opt = check_name options name in |
|
73 |
if #typ opt = typ then opt |
|
51978 | 74 |
else error ("Ill-typed system option " ^ quote name ^ " : " ^ #typ opt ^ " vs. " ^ typ) |
51943 | 75 |
end; |
51942 | 76 |
|
77 |
||
56467 | 78 |
(* markup *) |
51943 | 79 |
|
56467 | 80 |
fun markup options (name, pos) = |
81 |
let |
|
82 |
val opt = |
|
83 |
check_name options name |
|
84 |
handle ERROR msg => error (msg ^ Position.here pos); |
|
85 |
val props = Position.def_properties_of (#pos opt); |
|
86 |
in Markup.properties props (Markup.entity Markup.system_optionN name) end; |
|
87 |
||
88 |
||
89 |
(* typ *) |
|
90 |
||
51943 | 91 |
fun typ options name = #typ (check_name options name); |
92 |
||
93 |
||
94 |
(* basic operations *) |
|
95 |
||
96 |
fun put T print name x (options as Options tab) = |
|
97 |
let val opt = check_type options name T |
|
56465 | 98 |
in Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = print x}) tab) end; |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
99 |
|
51943 | 100 |
fun get T parse options name = |
101 |
let val opt = check_type options name T in |
|
102 |
(case parse (#value opt) of |
|
103 |
SOME x => x |
|
104 |
| NONE => |
|
51978 | 105 |
error ("Malformed value for system option " ^ quote name ^ |
51943 | 106 |
" : " ^ T ^ " =\n" ^ quote (#value opt))) |
107 |
end; |
|
108 |
||
109 |
||
110 |
(* internal lookup and update *) |
|
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
111 |
|
51951
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51946
diff
changeset
|
112 |
val bool = get boolT (try Markup.parse_bool); |
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51946
diff
changeset
|
113 |
val int = get intT (try Markup.parse_int); |
51988 | 114 |
val real = get realT (try Markup.parse_real); |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
115 |
val string = get stringT SOME; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
116 |
|
51951
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51946
diff
changeset
|
117 |
val put_bool = put boolT Markup.print_bool; |
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51946
diff
changeset
|
118 |
val put_int = put intT Markup.print_int; |
51990 | 119 |
val put_real = put realT Markup.print_real; |
51943 | 120 |
val put_string = put stringT I; |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
121 |
|
51943 | 122 |
|
123 |
(* external updates *) |
|
124 |
||
125 |
fun check_value options name = |
|
126 |
let val opt = check_name options name in |
|
127 |
if #typ opt = boolT then ignore (bool options name) |
|
128 |
else if #typ opt = intT then ignore (int options name) |
|
129 |
else if #typ opt = realT then ignore (real options name) |
|
130 |
else if #typ opt = stringT then ignore (string options name) |
|
131 |
else () |
|
132 |
end; |
|
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
133 |
|
56465 | 134 |
fun declare {pos, name, typ, value} (Options tab) = |
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
135 |
let |
56465 | 136 |
val options' = |
137 |
(case Symtab.lookup tab name of |
|
138 |
SOME other => |
|
139 |
error ("Duplicate declaration of system option " ^ quote name ^ Position.here pos ^ |
|
140 |
Position.here (#pos other)) |
|
141 |
| NONE => Options (Symtab.update (name, {pos = pos, typ = typ, value = value}) tab)); |
|
51943 | 142 |
val _ = |
143 |
typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse |
|
56465 | 144 |
error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ ^ |
145 |
Position.here pos); |
|
51943 | 146 |
val _ = check_value options' name; |
147 |
in options' end; |
|
148 |
||
149 |
fun update name value (options as Options tab) = |
|
150 |
let |
|
151 |
val opt = check_name options name; |
|
56465 | 152 |
val options' = |
153 |
Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = value}) tab); |
|
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
154 |
val _ = check_value options' name; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
155 |
in options' end; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
156 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
157 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
158 |
(* decode *) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
159 |
|
56465 | 160 |
fun decode_opt body = |
161 |
let open XML.Decode |
|
162 |
in list (pair properties (pair string (pair string string))) end body |
|
163 |
|> map (fn (props, (name, (typ, value))) => |
|
164 |
{pos = Position.of_properties props, name = name, typ = typ, value = value}); |
|
165 |
||
166 |
fun decode body = fold declare (decode_opt body) empty; |
|
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
167 |
|
48698
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
168 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
169 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
170 |
(** global default **) |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
171 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
172 |
val global_default = Synchronized.var "Options.default" (NONE: T option); |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
173 |
|
51978 | 174 |
fun err_no_default () = error "Missing default for system options within Isabelle process"; |
51943 | 175 |
|
176 |
fun change_default f x y = |
|
177 |
Synchronized.change global_default |
|
178 |
(fn SOME options => SOME (f x y options) |
|
179 |
| NONE => err_no_default ()); |
|
180 |
||
48698
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
181 |
fun default () = |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
182 |
(case Synchronized.value global_default of |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
183 |
SOME options => options |
51943 | 184 |
| NONE => err_no_default ()); |
48698
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
185 |
|
56467 | 186 |
fun default_markup arg = markup (default ()) arg; |
51946 | 187 |
fun default_typ name = typ (default ()) name; |
51942 | 188 |
fun default_bool name = bool (default ()) name; |
189 |
fun default_int name = int (default ()) name; |
|
190 |
fun default_real name = real (default ()) name; |
|
191 |
fun default_string name = string (default ()) name; |
|
192 |
||
51943 | 193 |
val default_put_bool = change_default put_bool; |
194 |
val default_put_int = change_default put_int; |
|
195 |
val default_put_real = change_default put_real; |
|
196 |
val default_put_string = change_default put_string; |
|
197 |
||
198 |
fun get_default name = |
|
199 |
let val options = default () in get (typ options name) SOME options name end; |
|
200 |
val put_default = change_default update; |
|
201 |
||
48698
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
202 |
fun set_default options = Synchronized.change global_default (K (SOME options)); |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
203 |
fun reset_default () = Synchronized.change global_default (K NONE); |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
204 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
205 |
fun load_default () = |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
206 |
(case getenv "ISABELLE_PROCESS_OPTIONS" of |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
207 |
"" => () |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
208 |
| name => |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
209 |
let val path = Path.explode name in |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
210 |
(case try File.read path of |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
211 |
SOME s => (set_default (decode (YXML.parse_body s)); ignore (try File.rm path)) |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
212 |
| NONE => ()) |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
213 |
end); |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
214 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
215 |
val _ = load_default (); |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
216 |
|
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
217 |
end; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
218 |