1 theory Config |
1 theory Config |
2 imports Base |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section {* Configuration Options *} |
5 section {* Configuration Options *} |
6 |
6 |
7 |
7 |
8 text {* |
8 text {* |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 You would like to enhance your tool with options which can be changed later on |
10 You would like to enhance your tool with options that can be changed |
11 by the user.\smallskip |
11 by the user without having to resort to the ML-level.\smallskip |
12 |
12 |
13 {\bf Solution:} This can be achieved using configuration values.\smallskip |
13 {\bf Solution:} This can be achieved using configuration values.\smallskip |
14 |
14 |
15 *} |
15 Assume you want to control three values, say @{ML_text bval} containing a |
16 |
16 boolean, @{ML_text ival} containing an integer and @{ML_text sval} |
17 ML {* |
17 containing a string. These values can be declared on the ML-level by |
18 val (bvalue, setup_bvalue) = Attrib.config_bool "bvalue" false |
|
19 val (ivalue, setup_ivalue) = Attrib.config_int "ivalue" 0 |
|
20 val (svalue, setup_svalue) = Attrib.config_string "svalue" "some string" |
|
21 *} |
|
22 |
|
23 setup "setup_bvalue o setup_ivalue o setup_svalue" |
|
24 |
|
25 declare [[bvalue = true, ivalue = 3]] |
|
26 |
|
27 text {* |
|
28 Note that this works without introducing a new command to modify the |
|
29 configuration options. *} |
|
30 |
|
31 ML {* |
|
32 Config.get @{context} bvalue |
|
33 *} |
18 *} |
34 |
19 |
35 ML {* |
20 ML {* |
36 Config.get_thy @{theory} ivalue |
21 val (bval, setup_bval) = Attrib.config_bool "bval" false |
|
22 val (ival, setup_ival) = Attrib.config_int "ival" 0 |
|
23 val (sval, setup_sval) = Attrib.config_string "sval" "some string" |
37 *} |
24 *} |
38 |
25 |
39 setup {* Config.put_thy svalue "foo" *} |
26 text {* |
40 |
27 where each value is given a default. To enable these values, they need to |
41 ML {* |
28 be set up using |
42 Config.get @{context} svalue |
|
43 *} |
29 *} |
44 |
30 |
45 ML {* |
31 setup {* setup_bval *} |
46 let val ctxt = Config.map ivalue (fn i => i + 1) @{context} |
32 setup {* setup_ival *} |
47 in Config.get ctxt ivalue end |
33 |
|
34 text {* or on the ML-level *} |
|
35 |
|
36 ML {*setup_sval @{theory} |
|
37 *} |
|
38 |
|
39 text {* |
|
40 The user can now manipulate the values with the command |
|
41 *} |
|
42 |
|
43 declare [[bval = true, ival = 3]] |
|
44 |
|
45 text {* |
|
46 On the ML-level these values can be retrieved using the function @{ML Config.get}: |
|
47 |
|
48 @{ML_response [display] "Config.get @{context} bval" "true"} |
|
49 |
|
50 @{ML_response [display] "Config.get @{context} ival" "3"} |
|
51 |
|
52 The function @{ML Config.put} manipulates the values. For example |
|
53 |
|
54 @{ML_response [display] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"} |
|
55 |
|
56 The same can be achived using the command \isacommand{setup}. |
|
57 *} |
|
58 |
|
59 setup {* Config.put_thy sval "bar" *} |
|
60 |
|
61 text {* |
|
62 Then retrival of this value yields now |
|
63 |
|
64 @{ML_response [display] "Config.get @{context} sval" "\"bar\""} |
|
65 |
|
66 We can apply a function to a value using @{ML Config.map}. For example incrementing |
|
67 @{ML ival} can be done by |
|
68 |
|
69 @{ML_response [display] |
|
70 "let |
|
71 val ctxt = Config.map ival (fn i => i + 1) @{context} |
|
72 in |
|
73 Config.get ctxt ival |
|
74 end" "4"} |
|
75 |
|
76 \begin{readmore} |
|
77 For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. |
|
78 \end{readmore} |
|
79 |
48 *} |
80 *} |
49 |
81 |
50 |
82 |
51 text {* |
83 text {* |
52 Code: Pure/Isar/attrib.ML, Pure/config.ML |
|
53 |
84 |
54 Note: Avoid to use references for this purpose! |
85 Note: Avoid to use references for this purpose! |
55 *} |
86 *} |
56 |
87 |
57 end |
88 end |