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, say @{ML_text bval} containing a |
15 Assume you want to control three values, namely @{ML_text bval} containing a |
16 boolean, @{ML_text ival} containing an integer and @{ML_text sval} |
16 boolean, @{ML_text ival} containing an integer and @{ML_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 with |
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 using |
26 be set up by |
27 *} |
27 *} |
28 |
28 |
29 setup {* setup_bval *} |
29 setup {* setup_bval *} |
30 setup {* setup_ival *} |
30 setup {* setup_ival *} |
31 |
31 |