equal
deleted
inserted
replaced
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 with |
17 containing a string. These values can be declared on the ML-level with |
18 *} |
18 *} |
19 |
19 |
20 ML {* |
20 ML{*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 |
21 val (ival, setup_ival) = Attrib.config_int "ival" 0 |
23 val (sval, setup_sval) = Attrib.config_string "sval" "some string" |
22 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *} |
24 *} |
|
25 |
23 |
26 text {* |
24 text {* |
27 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 |
28 be set up using |
26 be set up using |
29 *} |
27 *} |
31 setup {* setup_bval *} |
29 setup {* setup_bval *} |
32 setup {* setup_ival *} |
30 setup {* setup_ival *} |
33 |
31 |
34 text {* or on the ML-level *} |
32 text {* or on the ML-level *} |
35 |
33 |
36 ML {* |
34 ML{*setup_sval @{theory} *} |
37 setup_sval @{theory} |
|
38 *} |
|
39 |
35 |
40 text {* |
36 text {* |
41 The user can now manipulate the values from within Isabelle with the command |
37 The user can now manipulate the values from within Isabelle with the command |
42 *} |
38 *} |
43 |
39 |