diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Recipes/Config.thy --- 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