CookBook/Recipes/Config.thy
changeset 72 7b8c4fe235aa
parent 69 19106a9975c1
child 74 f6f8f8ba1eb1
--- 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