--- a/ProgTutorial/Recipes/Antiquotes.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Wed May 22 13:24:30 2019 +0200
@@ -34,7 +34,7 @@
   @{text [display] \<open>@{ML_checked "a_piece_of_code"}\<close>}
 
   The code is checked by sending the ML-expression @{text [quotes] "val _ =
-  a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML \<open>ML_Context.eval_source_in\<close>} in Line 7 below). The complete code of the
+  a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML \<open>ML_Context.eval_in\<close>} in Line 8 below). The complete code of the
   document antiquotation is as follows:
 
 \<close>
@@ -59,40 +59,25 @@
 
 
 text \<open>
-  The parser @{ML \<open>(Scan.lift Args.name)\<close>} in Line 7 parses a string, in this
-  case the code, and then calls the function @{ML output_ml}. As mentioned
-  before, the parsed code is sent to the ML-compiler in Line 4 using the
+  The parser @{ML \<open>(Scan.lift Args.text_input)\<close>} in Line 15 parses a string, in this
+  case the code, and then we call the function @{ML output_ml}. As mentioned
+  before, the parsed code is sent to the ML-compiler in Line 8 using the
   function @{ML ml_val}, which constructs the appropriate ML-expression, and
   using @{ML \<open>eval_in\<close> in ML_Context}, which calls the compiler.  If the code is
-  ``approved'' by the compiler, then the output function @{ML \<open>output\<close> in
-  Document_Antiquotation} in the next line pretty prints the code. This function expects
-  that the code is a list of (pretty)strings where each string correspond to a
-  line in the output. Therefore the use of @{ML \<open>(space_explode "\\n" txt)\<close>
-  for txt} which produces such a list according to linebreaks.  There are a
+  ``approved'' by the compiler, then the output given to @{ML \<open>antiquotation_pretty_source\<close> in
+  Thy_Output} in the Line 15 pretty prints the code. This function expects
+  that the code is (pretty) string. There are a
   number of options for antiquotations that are observed by the function 
   @{ML \<open>output\<close> in Document_Antiquotation} when printing the code (including \<open>[display]\<close> 
-  and \<open>[quotes]\<close>). The function @{ML \<open>antiquotation_raw\<close> in Thy_Output} in 
-  Line 7 sets up the new document antiquotation.
+  and \<open>[quotes]\<close>). 
 
   \begin{readmore}
   For more information about options of document antiquotations see \rsccite{sec:antiq}).
   \end{readmore}
 
-  Since we used the argument @{ML \<open>Position.none\<close>}, the compiler cannot give specific 
-  information about the line number, in case an error is detected. We 
-  can improve the code above slightly by writing 
 \<close>
 
 text \<open>
-  where in Lines 1 and 2 the positional information is properly treated. The
-  parser @{ML Parse.position} encodes the positional information in the 
-  result.
-
-  We can now write \<open>@{ML_checked2 "2 + 3"}\<close> in a document in order to
-  obtain @{ML_checked "2 + 3"} and be sure that this code compiles until
-  somebody changes the definition of addition.
-
-
   The second document antiquotation we describe extends the first by a pattern
   that specifies what the result of the ML-code should be and checks the
   consistency of the actual result with the given pattern. For this we are
@@ -105,11 +90,7 @@
   give a partial specification by using ellipses. For example \<open>(\<dots>, \<dots>)\<close>
   for specifying a pair.  In order to check consistency between the pattern
   and the output of the code, we have to change the ML-expression that is sent 
-  to the compiler: in \<open>ML_checked2\<close> we sent the expression @{text [quotes]
-  "val _ = a_piece_of_code"} to the compiler; now the wildcard \<open>_\<close>
-  must be be replaced by the given pattern. However, we have to remove all
-  ellipses from it and replace them by @{text [quotes] "_"}. The following 
-  function will do this:
+  to the compiler: 
 \<close>
 
 ML%linenosgray\<open>fun ml_pat pat code =
@@ -122,7 +103,6 @@
   Next we add a response indicator to the result using:
 \<close>
 
-
 ML %grayML\<open>fun add_resp pat = map (fn s => "> " ^ s) pat\<close>
 
 text \<open>
@@ -151,9 +131,9 @@
 
 (* FIXME *)
 text \<open>
-  In comparison with \<open>ML_checked\<close>, we only changed the line about 
-  the compiler (Line~2), the lines about
-  the output (Lines 4 to 7) and the parser in the setup (Line 11). Now 
+  In comparison with \<open>ML_checked\<close>, we changed the line about 
+  the compiler (Lines 4 to 5), the lines about
+  the output (Lines 6 to 7 and 9) and the parser setup (Line 14). Now 
   you can write
  
   @{text [display] \<open>@{ML_resp [display] "true andalso false" "false"}\<close>}