diff -r 95b42288294e -r 438703674711 ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue May 21 14:37:39 2019 +0200
@@ -12,6 +12,27 @@
 fun prefix_lines prfx txt = 
   map (fn s => prfx ^ s) (split_lines txt)
 
+fun is_sep "\<dots>" = true
+  | is_sep s = Symbol.is_ascii_blank s; 
+
+fun scan_word sep =
+  Scan.many1 sep >> K NONE ||
+  Scan.many1 (fn s => not (sep s) andalso Symbol.not_eof s) >> (SOME o implode);
+
+fun split_words sep = Symbol.scanner "Bad text" (Scan.repeat (scan_word sep) >> map_filter I);
+
+fun explode_words sep = split_words sep o Symbol.explode;
+
+fun match_string sep pat str =
+  let
+    fun match [] _ = true
+      | match (p :: ps) s =
+          size p <= size s andalso
+            (case try (unprefix p) s of
+              SOME s' => match ps s'
+            | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
+  in match (explode_words sep pat) str end;
+
 fun ml_with_vars' ys txt = 
     implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]
 
@@ -70,14 +91,20 @@
   (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
    Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))) 
 
-fun output_ml_response ctxt src =
+fun output_ml_response ignore_pat ctxt (src, opat) =
 let 
   val res = eval_response ctxt src
+  val _ = writeln res
+  val cnt = YXML.content_of res
+  val pat = case opat of NONE => cnt 
+            | SOME p => p |>  Input.source_content 
+  val _ = if ignore_pat orelse Print_Mode.print_mode_active Latex.latexN orelse match_string is_sep pat cnt then () 
+          else error (cat_lines ["Substring:", pat, "not contained in:", cnt])
+  val out = if ignore_pat then cnt else pat
 in 
-  OutputTutorial.output ctxt ([Input.source_content src] @ [Library.prefix_lines "> " res])
+  OutputTutorial.output ctxt ([Input.source_content src] @ [Library.prefix_lines "> " out])
 end
 
-
 (* checks and prints a single ML-item and produces an index entry *)
 fun output_ml_ind ctxt (src, stru) =
 let 
@@ -149,11 +176,13 @@
 
 val single_arg = Scan.lift (Args.text_input)
 val two_args   = Scan.lift (Args.text_input -- Args.text_input)
+val maybe_two_args = Scan.lift (Args.text_input -- Scan.option Args.text_input)
 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
 val ml_setup = 
   Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml
-  #> Thy_Output.antiquotation_raw @{binding "ML_response"} single_arg output_ml_response
+  #> Thy_Output.antiquotation_raw @{binding "ML_response"} maybe_two_args (output_ml_response false)
+  #> Thy_Output.antiquotation_raw @{binding "ML_response_ignore"} maybe_two_args (output_ml_response true)
   #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind
   #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind
   #> Thy_Output.antiquotation_raw @{binding "ML_structure_ind"} single_arg output_struct_ind