equal
deleted
inserted
replaced
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 @{ML_text bval} containing a |
15 Assume you want to control three values, namely @{text bval} containing a |
16 boolean, @{ML_text ival} containing an integer and @{ML_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 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 |