41 |
41 |
42 text {* |
42 text {* |
43 On the ML-level these values can be retrieved using the |
43 On the ML-level these values can be retrieved using the |
44 function @{ML Config.get}: |
44 function @{ML Config.get}: |
45 |
45 |
46 @{ML_response [display] "Config.get @{context} bval" "true"} |
46 @{ML_response [display,gray] "Config.get @{context} bval" "true"} |
47 |
47 |
48 @{ML_response [display] "Config.get @{context} ival" "3"} |
48 @{ML_response [display,gray] "Config.get @{context} ival" "3"} |
49 |
49 |
50 The function @{ML Config.put} manipulates the values. For example |
50 The function @{ML Config.put} manipulates the values. For example |
51 |
51 |
52 @{ML_response [display] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"} |
52 @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"} |
53 |
53 |
54 The same can be achived using the command \isacommand{setup}. |
54 The same can be achived using the command \isacommand{setup}. |
55 *} |
55 *} |
56 |
56 |
57 setup {* Config.put_thy sval "bar" *} |
57 setup {* Config.put_thy sval "bar" *} |
58 |
58 |
59 text {* |
59 text {* |
60 The retrival of this value yields now |
60 The retrival of this value yields now |
61 |
61 |
62 @{ML_response [display] "Config.get @{context} sval" "\"bar\""} |
62 @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""} |
63 |
63 |
64 We can apply a function to a value using @{ML Config.map}. For example incrementing |
64 We can apply a function to a value using @{ML Config.map}. For example incrementing |
65 @{ML ival} can be done by |
65 @{ML ival} can be done by |
66 |
66 |
67 @{ML_response [display] |
67 @{ML_response [display,gray] |
68 "let |
68 "let |
69 val ctxt = Config.map ival (fn i => i + 1) @{context} |
69 val ctxt = Config.map ival (fn i => i + 1) @{context} |
70 in |
70 in |
71 Config.get ctxt ival |
71 Config.get ctxt ival |
72 end" "4"} |
72 end" "4"} |