diff -r 438703674711 -r 321e220a6baa ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue May 21 16:22:30 2019 +0200
@@ -40,27 +40,27 @@
     ML_Lex.read "fn " @ ML_Lex.read (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) @
     ML_Lex.read " => (" @ src @ ML_Lex.read ")"
 
-fun ml_with_struct (NONE) src = ML_Lex.read_source false src 
+fun ml_with_struct (NONE) src = ML_Lex.read_source src 
   | ml_with_struct (SOME st) src = 
-      ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source false src @ ML_Lex.read " end"
+      ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source src @ ML_Lex.read " end"
 
 fun ml_val vs stru txt = 
     txt |> ml_with_struct stru
         |> ml_with_vars vs 
 
 fun ml_pat pat lhs =
-  ML_Lex.read "val " @ ML_Lex.read_source false pat @ 
+  ML_Lex.read "val " @ ML_Lex.read_source pat @ 
   ML_Lex.read " = " @
-  ML_Lex.read_source false lhs 
+  ML_Lex.read_source lhs 
 
 
 fun ml_struct src = 
   ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @
-  ML_Lex.read_source false src @
+  ML_Lex.read_source src @
   ML_Lex.read " end"
 
 fun ml_type src = 
-  ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option"
+  ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source src @ ML_Lex.read ") option"
 
 (* eval function *)
 fun eval_fn ctxt prep exp =
@@ -71,7 +71,7 @@
 let 
   fun compute exp = 
      let 
-       val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source false exp @ 
+       val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source exp @ 
                    ML_Lex.read " in (raise ERROR (@{make_string} r); ()) end )"
        val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) input 
      in ""
@@ -85,7 +85,7 @@
 
 fun output_ml ctxt (src, (vs, stru)) =
   (eval_fn ctxt (ml_val vs stru) src; 
-   output ctxt (split_lines (Input.source_content src)))
+   output ctxt (split_lines (fst (Input.source_content src))))
  
 val parser_ml = Scan.lift (Args.text_input --
   (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
@@ -97,18 +97,18 @@
   val _ = writeln res
   val cnt = YXML.content_of res
   val pat = case opat of NONE => cnt 
-            | SOME p => p |>  Input.source_content 
+            | SOME p => p |>  fst o 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 "> " out])
+  OutputTutorial.output ctxt ([fst (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 
-  val txt = Input.source_content src
+  val (txt,_) = Input.source_content src
 in
   (eval_fn ctxt (ml_val [] stru) src; 
    case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
@@ -123,7 +123,7 @@
 (* checks and prints structures *)
 fun gen_output_struct outfn ctxt src = 
 let 
-  val txt = Input.source_content src
+  val (txt, _) = Input.source_content src
 in
   (eval_fn ctxt ml_struct src; 
    outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
@@ -135,7 +135,7 @@
 (* prints functors; no checks *)
 fun gen_output_funct outfn src = 
 let
-  val txt = Input.source_content src
+  val (txt, _) = Input.source_content src
 in
   (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
 end
@@ -146,7 +146,7 @@
 (* checks and prints types *)
 fun gen_output_type outfn ctxt src = 
 let 
-  val txt = Input.source_content src
+  val (txt, _) = Input.source_content src
 in
   (eval_fn ctxt ml_type src; 
    outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
@@ -160,19 +160,19 @@
 (* checks and expression against a result pattern *)
 fun output_response ctxt (lhs, pat) = 
     (eval_fn ctxt (ml_pat pat) lhs;
-     output ctxt ((prefix_lines "" (Input.source_content lhs)) @ 
-       (prefix_lines "> " (dots_pat (Input.source_content pat)))))
+     output ctxt ((prefix_lines "" (fst (Input.source_content lhs))) @ 
+       (prefix_lines "> " (dots_pat (fst (Input.source_content pat))))))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake ctxt (lhs, pat) = 
     (eval_fn ctxt (ml_val [] NONE) lhs;
-     output ctxt ( (split_lines (Input.source_content lhs)) @ 
-        (prefix_lines "> " (dots_pat (Input.source_content pat)))))
+     output ctxt ( (split_lines (fst (Input.source_content lhs))) @ 
+        (prefix_lines "> " (dots_pat (fst (Input.source_content pat))))))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun ouput_response_fake_both ctxt (lhs, pat) = 
-    (output ctxt ((split_lines (Input.source_content lhs)) @ 
-     (prefix_lines "> " (dots_pat (Input.source_content pat)))))
+    (output ctxt ((split_lines (fst (Input.source_content lhs))) @ 
+     (prefix_lines "> " (dots_pat (fst ((Input.source_content pat)))))))
 
 val single_arg = Scan.lift (Args.text_input)
 val two_args   = Scan.lift (Args.text_input -- Args.text_input)
@@ -202,7 +202,7 @@
 
 fun check_file_exists _ src =
 let
-  val txt = Input.source_content src
+  val (txt, _) = Input.source_content src
 in
   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
    then Latex.string (href_link txt)