61
|
1 |
theory Config
|
63
|
2 |
imports "../Base"
|
61
|
3 |
begin
|
|
4 |
|
119
|
5 |
section {* Configuration Options\label{rec:config} *}
|
61
|
6 |
|
|
7 |
text {*
|
|
8 |
{\bf Problem:}
|
63
|
9 |
You would like to enhance your tool with options that can be changed
|
|
10 |
by the user without having to resort to the ML-level.\smallskip
|
61
|
11 |
|
|
12 |
{\bf Solution:} This can be achieved using configuration values.\smallskip
|
|
13 |
|
168
|
14 |
Assume you want to control three values, say @{text bval} containing a
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
boolean, @{text ival} containing an integer and @{text sval}
|
168
|
16 |
containing a string. These values can be declared on the ML-level by
|
61
|
17 |
*}
|
|
18 |
|
69
|
19 |
ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
|
63
|
20 |
val (ival, setup_ival) = Attrib.config_int "ival" 0
|
69
|
21 |
val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
|
63
|
22 |
|
|
23 |
text {*
|
67
|
24 |
where each value needs to be given a default. To enable these values, they need to
|
168
|
25 |
be set up with
|
63
|
26 |
*}
|
|
27 |
|
|
28 |
setup {* setup_bval *}
|
|
29 |
setup {* setup_ival *}
|
|
30 |
|
191
|
31 |
text {* or on the ML-level with *}
|
63
|
32 |
|
69
|
33 |
ML{*setup_sval @{theory} *}
|
63
|
34 |
|
|
35 |
text {*
|
67
|
36 |
The user can now manipulate the values from within Isabelle with the command
|
61
|
37 |
*}
|
|
38 |
|
63
|
39 |
declare [[bval = true, ival = 3]]
|
|
40 |
|
|
41 |
text {*
|
67
|
42 |
On the ML-level these values can be retrieved using the
|
65
|
43 |
function @{ML Config.get}:
|
63
|
44 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
@{ML_response [display,gray] "Config.get @{context} bval" "true"}
|
61
|
46 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
@{ML_response [display,gray] "Config.get @{context} ival" "3"}
|
63
|
48 |
|
|
49 |
The function @{ML Config.put} manipulates the values. For example
|
|
50 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
51 |
@{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}
|
63
|
52 |
|
168
|
53 |
The same can be achieved using the command \isacommand{setup}.
|
61
|
54 |
*}
|
|
55 |
|
63
|
56 |
setup {* Config.put_thy sval "bar" *}
|
|
57 |
|
|
58 |
text {*
|
191
|
59 |
Now the retrieval of this value yields:
|
63
|
60 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
@{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""}
|
63
|
62 |
|
|
63 |
We can apply a function to a value using @{ML Config.map}. For example incrementing
|
168
|
64 |
@{ML ival} can be done by:
|
63
|
65 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
@{ML_response [display,gray]
|
63
|
67 |
"let
|
191
|
68 |
val ctxt' = Config.map ival (fn i => i + 1) @{context}
|
63
|
69 |
in
|
191
|
70 |
Config.get ctxt' ival
|
63
|
71 |
end" "4"}
|
|
72 |
|
68
|
73 |
\begin{readmore}
|
63
|
74 |
For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
|
68
|
75 |
\end{readmore}
|
63
|
76 |
|
68
|
77 |
There are many good reasons to control parameters in this way. One is
|
191
|
78 |
that no global reference is needed, which would cause many headaches
|
|
79 |
with the multithreaded execution of Isabelle.
|
|
80 |
*}
|
|
81 |
|
61
|
82 |
end |