equal
deleted
inserted
replaced
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, say @{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 by |
17 containing a string. These values can be declared on the ML-level with |
18 *} |
18 *} |
19 |
19 |
20 ML {* |
20 ML {* |
21 val (bval, setup_bval) = Attrib.config_bool "bval" false |
21 val (bval, setup_bval) = Attrib.config_bool "bval" false |
22 val (ival, setup_ival) = Attrib.config_int "ival" 0 |
22 val (ival, setup_ival) = Attrib.config_int "ival" 0 |
23 val (sval, setup_sval) = Attrib.config_string "sval" "some string" |
23 val (sval, setup_sval) = Attrib.config_string "sval" "some string" |
24 *} |
24 *} |
25 |
25 |
26 text {* |
26 text {* |
27 where each value is given a default. To enable these values, they need to |
27 where each value needs to be given a default. To enable these values, they need to |
28 be set up using |
28 be set up using |
29 *} |
29 *} |
30 |
30 |
31 setup {* setup_bval *} |
31 setup {* setup_bval *} |
32 setup {* setup_ival *} |
32 setup {* setup_ival *} |
36 ML {* |
36 ML {* |
37 setup_sval @{theory} |
37 setup_sval @{theory} |
38 *} |
38 *} |
39 |
39 |
40 text {* |
40 text {* |
41 The user can now manipulate the values with the command |
41 The user can now manipulate the values from within Isabelle with the command |
42 *} |
42 *} |
43 |
43 |
44 declare [[bval = true, ival = 3]] |
44 declare [[bval = true, ival = 3]] |
45 |
45 |
46 text {* |
46 text {* |
47 from within Isabelle. On the ML-level these values can be retrieved using the |
47 On the ML-level these values can be retrieved using the |
48 function @{ML Config.get}: |
48 function @{ML Config.get}: |
49 |
49 |
50 @{ML_response [display] "Config.get @{context} bval" "true"} |
50 @{ML_response [display] "Config.get @{context} bval" "true"} |
51 |
51 |
52 @{ML_response [display] "Config.get @{context} ival" "3"} |
52 @{ML_response [display] "Config.get @{context} ival" "3"} |