--- a/CookBook/Recipes/Config.thy	Wed Jan 07 16:36:31 2009 +0000
+++ b/CookBook/Recipes/Config.thy	Thu Jan 08 22:46:06 2009 +0000
@@ -1,5 +1,5 @@
 theory Config
-imports Base
+imports "../Base"
 begin
 
 section {* Configuration Options *} 
@@ -7,49 +7,80 @@
 
 text {*
   {\bf Problem:} 
-  You would like to enhance your tool with options which can be changed later on
-  by the user.\smallskip
+  You would like to enhance your tool with options that can be changed 
+  by the user without having to resort to the ML-level.\smallskip
 
   {\bf Solution:} This can be achieved using configuration values.\smallskip
 
-  *}
-
-ML {*
-val (bvalue, setup_bvalue) = Attrib.config_bool "bvalue" false
-val (ivalue, setup_ivalue) = Attrib.config_int "ivalue" 0
-val (svalue, setup_svalue) = Attrib.config_string "svalue" "some string"
-*}
-
-setup "setup_bvalue o setup_ivalue o setup_svalue"
-
-declare [[bvalue = true, ivalue = 3]]
-
-text {*
-  Note that this works without introducing a new command to modify the 
-  configuration options. *}
-
-ML {*
-Config.get @{context} bvalue
+  Assume you want to control three values, say @{ML_text bval} containing a
+  boolean,  @{ML_text ival} containing an integer and @{ML_text sval} 
+  containing a string. These values can be declared on the ML-level by
 *}
 
 ML {*
-Config.get_thy @{theory} ivalue
+val (bval, setup_bval) = Attrib.config_bool "bval" false
+val (ival, setup_ival) = Attrib.config_int "ival" 0
+val (sval, setup_sval) = Attrib.config_string "sval" "some string"
+*}
+
+text {* 
+  where each value is given a default. To enable these values, they need to 
+  be set up using 
+*}
+
+setup {* setup_bval *} 
+setup {* setup_ival *}
+
+text {* or on the ML-level *}
+
+ML {*setup_sval @{theory} 
+*}
+
+text {*
+  The user can now manipulate the values with the command
 *}
 
-setup {* Config.put_thy svalue "foo" *}
+declare [[bval = true, ival = 3]]
+
+text {*
+  On the ML-level these values can be retrieved using the function @{ML Config.get}:
+
+  @{ML_response [display] "Config.get @{context} bval" "true"}
 
-ML {* 
-Config.get @{context} svalue
+  @{ML_response [display] "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"}
+
+  The same can be achived using the command \isacommand{setup}.
 *}
 
-ML {*
-let val ctxt = Config.map ivalue (fn i => i + 1) @{context}
-in Config.get ctxt ivalue end
+setup {* Config.put_thy sval "bar" *}
+
+text {* 
+  Then retrival of this value yields now
+
+  @{ML_response [display] "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] 
+"let 
+  val ctxt = Config.map ival (fn i => i + 1) @{context}
+in 
+  Config.get ctxt ival
+end" "4"}
+
+\begin{readmore}
+  For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
+\end{readmore}
+
 *}
 
 
 text {*
-  Code: Pure/Isar/attrib.ML, Pure/config.ML
 
   Note: Avoid to use references for this purpose!
   *}

--- a/CookBook/Recipes/NamedThms.thy	Wed Jan 07 16:36:31 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Thu Jan 08 22:46:06 2009 +0000
@@ -47,18 +47,21 @@
 
 declare rule1[foo del]
 
-text {* and query the remaining ones by: *}
+text {* and query the remaining ones with:
 
-thm foo
+@{ML_response_fake_both [display] "thm foo" 
+"?C
+?B"}
 
-text {* 
   On the ML-level the rules marked with @{text "foo"} an be retrieved
   using the function @{ML FooRules.get}:
 
   @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
 
   \begin{readmore}
-  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
+  For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
+  the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
+  data.
   \end{readmore}
  *}
 

--- a/CookBook/Recipes/StoringData.thy	Wed Jan 07 16:36:31 2009 +0000
+++ b/CookBook/Recipes/StoringData.thy	Thu Jan 08 22:46:06 2009 +0000
@@ -2,7 +2,7 @@
 imports "../Base"
 begin
 
-section {* Storing Data *} 
+section {* Storing Data\label{recipe:storingdata} *} 
 
 
 text {*
@@ -16,8 +16,7 @@
 
   *}
 
-ML {*
-local
+ML {* local
 
 structure Data = GenericDataFun
 (
@@ -33,8 +32,7 @@
 
 fun update k v = Data.map (Symtab.update (k, v))
 
-end
-*}
+end *}
 
 setup {* Context.theory_map (update "foo" 1) *}
 

--- a/CookBook/Recipes/TimeLimit.thy	Wed Jan 07 16:36:31 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Thu Jan 08 22:46:06 2009 +0000
@@ -1,41 +1,54 @@
 theory TimeLimit
-imports Base
+imports "../Base"
 begin
 
 section {* Restricting the Runtime of a Function *} 
 
-
 text {*
   {\bf Problem:}
-  Your tool should run only a specified amount of seconds.\smallskip
+  Your tool should run only a specified amount of time.\smallskip
 
-  {\bf Solution:} This can be achieved using time limits.\smallskip
+  {\bf Solution:} This can be achieved using the function 
+  @{ML timeLimit in TimeLimit}.\smallskip
 
-  Assume the following function should run only five seconds:
+  Assume the following well-known function:
 
   *}
 
-ML {*
+ML {* 
 fun ackermann (0, n) = n + 1
   | ackermann (m, 0) = ackermann (m - 1, 1)
   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))
 *}
 
-ML {* ackermann (3, 12) *}
+text {*
+
+  Now the call 
+
+  @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"}
 
-(* takes more than 10 seconds *)
+  takes a bit long. To avoid this, the call can be encapsulated 
+  in a time limit of five seconds. For this you have to write:
+
+@{ML_response [display]
+"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 
+  handle TimeOut => ~1"
+"~1"}
 
-text {*
-  The call can be encapsulated in a time limit of five seconds as follows:
-  *}
+  where @{ML_text TimeOut} is the exception raised when the time limit
+  is reached.
+
+  Note that @{ML  "timeLimit" in TimeLimit} is only meaningful when you use PolyML, 
+  because PolyML has a rich infrastructure for multithreading programming on 
+  which @{ML "timeLimit" in TimeLimit} relies.
 
-ML {* 
-TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (3, 12) 
-  handle TimeOut => ~1
+\begin{readmore}
+   The function @{ML "timeLimit" in TimeLimit} is defined in the structure
+  @{ML_struct TimeLimit} which can be found in the file 
+  @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}.
+\end{readmore}
+
+ 
 *}
 
-text {*
-  The function "TimeLimit.timeLimit" has type "???" and is defined in
-  TODO: refer to code *}
-
 end
\ No newline at end of file