--- a/CookBook/Recipes/Antiquotes.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/Recipes/Antiquotes.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -1,24 +1,31 @@
 
 theory Antiquotes
-imports Main
+imports "../Base"
 begin
 
 
-section {* Two Document Antiquotations *}
+section {* Useful Document Antiquotations *}
 
 text {*
+  {\bf Problem:} 
+  How to keep ML-code included in a document in sync with the actual code.\smallskip
 
-  For writing documents using Isabelle it is often uesful to use
-  document antiquotations. Below we give the code for such an 
-  antiquotation that typesets ML-code and also checks whether
-  the code is actually correct. In this way one can achieve that the
-  document is always in sync with code.
+  {\bf Solution:} This can be achieved using document antiquotations.\smallskip
+
+  Document antiquotations are a convenient method for type-setting consitently 
+  a group of items in a document. They can also be used for sophisticated
+  \LaTeX hacking.  
 
-  Below we introduce the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which
-  takes a piece of code as argument. We will check this code by sending 
-  the ML-expression @{text "val _ = \<dots>"} to the ML-compiler (i.e.~the 
-  function @{ML "ML_Context.eval_in"}). The code for this antiquotation
-  is as follows:
+  Below we give the code for two such 
+  antiquotations that can be used to typeset ML-code and also to check whether
+  the code is actually compiles. In this way one can relatively easily 
+  keep documents in sync with code.
+
+  We first describe the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which
+  takes a piece of code as argument. This code is checked by sending 
+  the ML-expression @{text "val _ = \<dots>"} containing the given code to the 
+  ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"}). The code 
+  for this antiquotation is as follows:
 *}
 
 ML {*
@@ -26,7 +33,8 @@
 
 fun output_ml ml src ctxt txt =
   (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt);
-  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))
+  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
+                                            (space_explode "\n" txt))
 
 val _ = ThyOutput.add_commands
  [("ML_checked", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val))]
@@ -37,21 +45,25 @@
   Note that the parser @{ML "(Scan.lift Args.name)"} parses a string. If the
   code is approved by the compiler, the output function 
   @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"}
-  pretty prints the code. There are a number of options that are observed
-  when printing the code (for example @{text "[display]"}; for more information
-  about the options see \rsccite{sec:antiq}).
+  pretty prints the code. This function expects that the code is a list of strings
+  according to the line breaks (therefore the 
+  @{ML_open "(space_explode \"\\n\" txt)" for txt} which produces this list).
+  There are a number of options that are observed by @{ML ThyOutput.output_list}
+  when printing the code (for example @{text "[display]"} and @{text "[source]"}; 
+  for more information about these options see \rsccite{sec:antiq}).
 
-  Since we
-  used the argument @{ML "Position.none"}, the compiler cannot give specific 
+  Since we used the argument @{ML "Position.none"}, the compiler cannot give specific 
   information about the line number where an error might have occurred. We 
   can improve this code slightly by writing 
 
+  The second 
 *}
 
 ML {*
 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))
+  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
+                                            (space_explode "\n" txt))
 
 val _ = ThyOutput.add_commands
  [("ML_checked", ThyOutput.args 
@@ -59,16 +71,12 @@
 *}
 
 text {*
-  where the antiquotation can also handle position information.
-
   (FIXME: say something about OuterParse.position)
-
 *}
 
 ML {*
-
 fun ml_pat (rhs, pat) =
-  let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
+  let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
   in
     "val " ^ pat' ^ " = " ^ rhs
   end;
@@ -80,7 +88,6 @@
   (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat));
   let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
   in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
-
 *}