--- a/CookBook/Recipes/Antiquotes.thy	Tue Dec 16 17:37:39 2008 +0100
+++ b/CookBook/Recipes/Antiquotes.thy	Tue Dec 16 17:28:05 2008 +0000
@@ -21,12 +21,12 @@
   provides a sanity check for the code and also allows one to keep documents
   in sync with other code, for example Isabelle.
 
-  We first describe the antiquotation @{text "@{ML_checked \"\<dots>\"}"}. This
-  antiquotation takes a piece of code as argument; this code is then checked
+  We first describe the antiquotation @{text "@{ML_checked \"expr\"}"}. This
+  antiquotation takes a piece of code as argument. The argument is checked
   by sending the ML-expression @{text [quotes] "val _ = \<dots>"} containing the
-  given code to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"}
-  in the snippet below). The code for @{text "@{ML_checked \"\<dots>\"}"} is as
-  follows:
+  given argument to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"}
+  in Line 4 in the code below). The code of @{text "@{ML_checked \"expr\"}"} 
+  is as follows:
 
 *}
 
@@ -44,12 +44,12 @@
 text {*
 
   Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, 
-  in this case the code. This code is send to the ML-compiler in the line 4.  
+  in this case the code given as argument. This argument is send to the ML-compiler in the line 4.  
   If the code is ``approved'' by the compiler, then the output function @{ML
   "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the
   code. This function expects that the code is a list of strings where each
-  string correspond to a line (therefore the @{ML "(space_explode \"\\n\" txt)" for txt} 
-  which produces this list).  There are a number of options for antiquotations
+  string correspond to a line. Therefore the @{ML "(space_explode \"\\n\" txt)" for txt} 
+  which produces this list.  There are a number of options for antiquotations
   that are observed by @{ML ThyOutput.output_list} when printing the code (for
   example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}).
 
@@ -63,8 +63,7 @@
 
 *}
 
-ML {*
-fun output_ml ml src ctxt (txt,pos) =
+ML %linenumbers {* fun output_ml ml src ctxt (txt,pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
                                             (space_explode "\n" txt))
@@ -75,35 +74,40 @@
 *}
 
 text {*
+  where in Lines 1 and 2 the positional information is properly treated.
+
   (FIXME: say something about OuterParse.position)
 
   We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to
   obtain @{ML_checked "2 + 3"} and be sure that this code compiles until
-  somebody changes the definition of @{ML "(op +)"}.
+  somebody changes the definition of \mbox{@{ML "(op +)"}}.
 
 
-  The second antiquotation extends the first by allowing to also give
-  hints what the result of the ML-code is and check consistency of these
-  hints. For this we use the antiquotation  @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"}
-  whose first argument is the ML-code and the second is the result. 
+  The second antiquotation extends the first by allowing also to give
+  hints what the result of the ML-code is and check the consistency of 
+  the actual result with these hints. For this we use the antiquotation  
+  @{text "@{ML_response \"expr\" \"pat\"}"}
+  whose first argument is the ML-code and the second is a pattern specifying
+  the result. To add some convenience we allow the user to give a partial
+  specification using @{text "\<dots>"}.
 
-  In the antiquotation @{text "@{ML_checked \"\<dots>\"}"} we send the expresion 
-  @{text [quotes] "val _ = \<dots>"} to the compiler. Now we will use the hints
-  to construct a pattern for the @{text "_"}. To add some convenince we allow
-  the user to give partial hints using @{text "\<dots>"}, which however need to
-  be replaced by @{text "_"} before sending the code to the compiler. The
-  function 
+  In the antiquotation @{text "@{ML_checked \"expr\"}"} we send the expression 
+  @{text [quotes] "val _ = expr"} to the compiler. Instead of the wildcard
+  @{text "_"}, we will here use the hints to construct a proper pattern. To
+  do this we need to replace the @{text "\<dots>"} by @{text "_"} before sending the 
+  code to the compiler. The function 
 
 *}
 
-ML {*
+ML {* 
 fun ml_pat (rhs, pat) =
 let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
 in "val " ^ pat' ^ " = " ^ rhs end;
 *}
 
 text {* 
-  will do this. Next we like to add a response indicator to the result using:
+  will construct the pattern that the compiler can use. Next we like to add 
+  a response indicator to the result using:
 *}
 
 
@@ -152,7 +156,6 @@
 *}
 
 
-
 end