10 You would like to enhance your tool with options that can be changed |
10 You would like to enhance your tool with options that can be changed |
11 by the user without having to resort to the ML-level.\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 Assume you want to control three values, namely @{text bval} containing a |
15 Assume you want to control three values, say @{text bval} containing a |
16 boolean, @{text ival} containing an integer and @{text sval} |
16 boolean, @{text ival} containing an integer and @{text sval} |
17 containing a string. These values can be declared on the ML-level with |
17 containing a string. These values can be declared on the ML-level by |
18 *} |
18 *} |
19 |
19 |
20 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false |
20 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false |
21 val (ival, setup_ival) = Attrib.config_int "ival" 0 |
21 val (ival, setup_ival) = Attrib.config_int "ival" 0 |
22 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *} |
22 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *} |
23 |
23 |
24 text {* |
24 text {* |
25 where each value needs to be given a default. To enable these values, they need to |
25 where each value needs to be given a default. To enable these values, they need to |
26 be set up by |
26 be set up with |
27 *} |
27 *} |
28 |
28 |
29 setup {* setup_bval *} |
29 setup {* setup_bval *} |
30 setup {* setup_ival *} |
30 setup {* setup_ival *} |
31 |
31 |
49 |
49 |
50 The function @{ML Config.put} manipulates the values. For example |
50 The function @{ML Config.put} manipulates the values. For example |
51 |
51 |
52 @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"} |
52 @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"} |
53 |
53 |
54 The same can be achived using the command \isacommand{setup}. |
54 The same can be achieved using the command \isacommand{setup}. |
55 *} |
55 *} |
56 |
56 |
57 setup {* Config.put_thy sval "bar" *} |
57 setup {* Config.put_thy sval "bar" *} |
58 |
58 |
59 text {* |
59 text {* |
60 The retrival of this value yields now |
60 Now the retrival of this value yields: |
61 |
61 |
62 @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""} |
62 @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""} |
63 |
63 |
64 We can apply a function to a value using @{ML Config.map}. For example incrementing |
64 We can apply a function to a value using @{ML Config.map}. For example incrementing |
65 @{ML ival} can be done by |
65 @{ML ival} can be done by: |
66 |
66 |
67 @{ML_response [display,gray] |
67 @{ML_response [display,gray] |
68 "let |
68 "let |
69 val ctxt = Config.map ival (fn i => i + 1) @{context} |
69 val ctxt = Config.map ival (fn i => i + 1) @{context} |
70 in |
70 in |