|
1 (* Title: Pure/config.ML |
|
2 ID: $Id$ |
|
3 Author: Makarius |
|
4 |
|
5 Configuration options as values within the local context. Global |
|
6 environment of named options, with type declaration. |
|
7 *) |
|
8 |
|
9 signature CONFIG = |
|
10 sig |
|
11 type 'a T |
|
12 val get: Proof.context -> 'a T -> 'a |
|
13 val get_thy: theory -> 'a T -> 'a |
|
14 val get_generic: Context.generic -> 'a T -> 'a |
|
15 val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context |
|
16 val map_thy: 'a T -> ('a -> 'a) -> theory -> theory |
|
17 val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic |
|
18 val put: 'a T -> 'a -> Proof.context -> Proof.context |
|
19 val put_thy: 'a T -> 'a -> theory -> theory |
|
20 val put_generic: 'a T -> 'a -> Context.generic -> Context.generic |
|
21 val put_generic_src: string -> string -> Context.generic -> Context.generic |
|
22 val print_configs: Proof.context -> unit |
|
23 val bool: string -> bool -> bool T |
|
24 val int: string -> int -> int T |
|
25 val string: string -> string -> string T |
|
26 end; |
|
27 |
|
28 structure Config: CONFIG = |
|
29 struct |
|
30 |
|
31 (* abstract configuration options *) |
|
32 |
|
33 datatype 'a T = Config of |
|
34 {get_value: Context.generic -> 'a, |
|
35 map_value: ('a -> 'a) -> Context.generic -> Context.generic}; |
|
36 |
|
37 fun get_generic context (Config {get_value, ...}) = get_value context; |
|
38 fun get_ctxt ctxt = get_generic (Context.Proof ctxt); |
|
39 fun get_thy thy = get_generic (Context.Theory thy); |
|
40 |
|
41 fun map_generic (Config {map_value, ...}) f context = map_value f context; |
|
42 fun map_ctxt config f = Context.proof_map (map_generic config f); |
|
43 fun map_thy config f = Context.theory_map (map_generic config f); |
|
44 |
|
45 fun put_generic config value = map_generic config (K value); |
|
46 fun put_ctxt config value = map_ctxt config (K value); |
|
47 fun put_thy config value = map_thy config (K value); |
|
48 |
|
49 |
|
50 (* mixed values *) |
|
51 |
|
52 datatype value = |
|
53 Bool of bool | |
|
54 Int of int | |
|
55 String of string; |
|
56 |
|
57 fun read_value (Bool _) "true" = SOME (Bool true) |
|
58 | read_value (Bool _) "false" = SOME (Bool false) |
|
59 | read_value (Int _) s = Option.map Int (Syntax.read_int s) |
|
60 | read_value (String _) s = SOME (String s); |
|
61 |
|
62 fun print_value (Bool true) = "true" |
|
63 | print_value (Bool false) = "false" |
|
64 | print_value (Int i) = signed_string_of_int i |
|
65 | print_value (String s) = quote s; |
|
66 |
|
67 fun print_type (Bool _) = "boolean" |
|
68 | print_type (Int _) = "integer" |
|
69 | print_type (String _) = "string"; |
|
70 |
|
71 structure ConfigData = GenericDataFun |
|
72 ( |
|
73 type T = value Inttab.table; |
|
74 val empty = Inttab.empty; |
|
75 val extend = I; |
|
76 fun merge _ = Inttab.merge (K true); |
|
77 ); |
|
78 |
|
79 |
|
80 (* global declarations *) |
|
81 |
|
82 local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in |
|
83 |
|
84 fun put_generic_src name src_value context = |
|
85 (case Symtab.lookup (! global_configs) name of |
|
86 NONE => error ("Unknown configuration option " ^ quote name) |
|
87 | SOME (config, default) => |
|
88 (case read_value default src_value of |
|
89 SOME value => put_generic config value context |
|
90 | NONE => error ("Malformed " ^ print_type default ^ |
|
91 " value for configuration option " ^ quote name))); |
|
92 |
|
93 fun declare make dest name default = |
|
94 let |
|
95 val id = serial (); |
|
96 |
|
97 val default_value = make default; |
|
98 fun get_value context = |
|
99 the_default default_value (Inttab.lookup (ConfigData.get context) id); |
|
100 fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) f); |
|
101 val config_value = Config {get_value = get_value, map_value = map_value}; |
|
102 |
|
103 val _ = CRITICAL (fn () => |
|
104 (if Symtab.defined (! global_configs) name |
|
105 then warning ("Hiding existing configuration option " ^ quote name) else (); |
|
106 change global_configs (Symtab.update (name, (config_value, default_value))))); |
|
107 |
|
108 in Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} end; |
|
109 |
|
110 fun print_configs ctxt = |
|
111 let |
|
112 fun prt (name, (config, default)) = |
|
113 Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1, |
|
114 Pretty.str (print_value (get_ctxt ctxt config))]; |
|
115 val configs = sort_wrt #1 (Symtab.dest (! global_configs)); |
|
116 in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; |
|
117 |
|
118 end; |
|
119 |
|
120 val bool = declare Bool (fn Bool b => b); |
|
121 val int = declare Int (fn Int i => i); |
|
122 val string = declare String (fn String s => s); |
|
123 |
|
124 |
|
125 (*final declarations of this structure!*) |
|
126 val get = get_ctxt; |
|
127 val map = map_ctxt; |
|
128 val put = put_ctxt; |
|
129 |
|
130 end; |