equal
deleted
inserted
replaced
31 setup {* setup_bval *} |
31 setup {* setup_bval *} |
32 setup {* setup_ival *} |
32 setup {* setup_ival *} |
33 |
33 |
34 text {* or on the ML-level *} |
34 text {* or on the ML-level *} |
35 |
35 |
36 ML {*setup_sval @{theory} |
36 ML {* |
|
37 setup_sval @{theory} |
37 *} |
38 *} |
38 |
39 |
39 text {* |
40 text {* |
40 The user can now manipulate the values with the command |
41 The user can now manipulate the values with the command |
41 *} |
42 *} |
42 |
43 |
43 declare [[bval = true, ival = 3]] |
44 declare [[bval = true, ival = 3]] |
44 |
45 |
45 text {* |
46 text {* |
46 On the ML-level these values can be retrieved using the function @{ML Config.get}: |
47 from within Isabelle. On the ML-level these values can be retrieved using the |
|
48 function @{ML Config.get}: |
47 |
49 |
48 @{ML_response [display] "Config.get @{context} bval" "true"} |
50 @{ML_response [display] "Config.get @{context} bval" "true"} |
49 |
51 |
50 @{ML_response [display] "Config.get @{context} ival" "3"} |
52 @{ML_response [display] "Config.get @{context} ival" "3"} |
51 |
53 |
57 *} |
59 *} |
58 |
60 |
59 setup {* Config.put_thy sval "bar" *} |
61 setup {* Config.put_thy sval "bar" *} |
60 |
62 |
61 text {* |
63 text {* |
62 Then retrival of this value yields now |
64 The retrival of this value yields now |
63 |
65 |
64 @{ML_response [display] "Config.get @{context} sval" "\"bar\""} |
66 @{ML_response [display] "Config.get @{context} sval" "\"bar\""} |
65 |
67 |
66 We can apply a function to a value using @{ML Config.map}. For example incrementing |
68 We can apply a function to a value using @{ML Config.map}. For example incrementing |
67 @{ML ival} can be done by |
69 @{ML ival} can be done by |