--- a/CookBook/Recipes/Config.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Recipes/Config.thy Wed Jan 14 23:44:14 2009 +0000
@@ -43,13 +43,13 @@
On the ML-level these values can be retrieved using the
function @{ML Config.get}:
- @{ML_response [display] "Config.get @{context} bval" "true"}
+ @{ML_response [display,gray] "Config.get @{context} bval" "true"}
- @{ML_response [display] "Config.get @{context} ival" "3"}
+ @{ML_response [display,gray] "Config.get @{context} ival" "3"}
The function @{ML Config.put} manipulates the values. For example
- @{ML_response [display] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}
+ @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}
The same can be achived using the command \isacommand{setup}.
*}
@@ -59,12 +59,12 @@
text {*
The retrival of this value yields now
- @{ML_response [display] "Config.get @{context} sval" "\"bar\""}
+ @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""}
We can apply a function to a value using @{ML Config.map}. For example incrementing
@{ML ival} can be done by
- @{ML_response [display]
+ @{ML_response [display,gray]
"let
val ctxt = Config.map ival (fn i => i + 1) @{context}
in