author | wenzelm |
Mon, 10 Sep 2012 17:13:17 +0200 | |
changeset 49246 | 248e66e8321f |
parent 48698 | 2585042b1a30 |
child 51942 | 527e39becafc |
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 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
4 |
Stand-alone options with external string representation. |
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 |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
9 |
type T |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
10 |
val empty: T |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
11 |
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
|
12 |
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
|
13 |
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
|
14 |
val string: T -> string -> string |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
15 |
val declare: {name: string, typ: string, value: string} -> T -> T |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
16 |
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
|
17 |
val default: unit -> T |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
18 |
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
|
19 |
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
|
20 |
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
|
21 |
end; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
22 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
23 |
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
|
24 |
struct |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
25 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
26 |
(* representation *) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
27 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
28 |
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
|
29 |
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
|
30 |
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
|
31 |
val stringT = "string"; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
32 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
33 |
datatype T = Options of {typ: string, value: string} Symtab.table; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
34 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
35 |
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
|
36 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
37 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
38 |
(* get *) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
39 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
40 |
fun get T parse (Options tab) name = |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
41 |
(case Symtab.lookup tab name of |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
42 |
SOME {typ, value} => |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
43 |
if typ = T then |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
44 |
(case parse value of |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
45 |
SOME x => x |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
46 |
| NONE => |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
47 |
error ("Malformed value for option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote value)) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
48 |
else error ("Ill-typed option " ^ quote name ^ " : " ^ typ ^ " vs. " ^ T) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
49 |
| NONE => error ("Unknown option " ^ quote name)); |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
50 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
51 |
val bool = get boolT Bool.fromString; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
52 |
val int = get intT Int.fromString; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
53 |
val real = get realT Real.fromString; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
54 |
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
|
55 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
56 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
57 |
(* declare *) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
58 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
59 |
fun declare {name, typ, value} (Options tab) = |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
60 |
let |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
61 |
val check_value = |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
62 |
if typ = boolT then ignore oo bool |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
63 |
else if typ = intT then ignore oo int |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
64 |
else if typ = realT then ignore oo real |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
65 |
else if typ = stringT then ignore oo string |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
66 |
else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ); |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
67 |
val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
68 |
handle Symtab.DUP _ => error ("Duplicate declaration of option " ^ quote name); |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
69 |
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
|
70 |
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
|
71 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
72 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
73 |
(* decode *) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
74 |
|
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
75 |
fun decode body = |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
76 |
fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value})) |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
77 |
(let open XML.Decode in list (triple string string string) end body) empty; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
78 |
|
48698
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
79 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
80 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
81 |
(** global default **) |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
82 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
83 |
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
|
84 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
85 |
fun default () = |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
86 |
(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
|
87 |
SOME options => options |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
88 |
| NONE => error "No global default options"); |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
89 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
93 |
fun load_default () = |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
94 |
(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
|
95 |
"" => () |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
96 |
| name => |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
97 |
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
|
98 |
(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
|
99 |
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
|
100 |
| NONE => ()) |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
101 |
end); |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
102 |
|
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
103 |
val _ = load_default (); |
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48456
diff
changeset
|
104 |
|
48456
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
105 |
end; |
d8ff14f44a40
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
diff
changeset
|
106 |