--- a/ProgTutorial/Base.thy	Tue May 14 13:39:31 2019 +0200
+++ b/ProgTutorial/Base.thy	Tue May 14 16:59:53 2019 +0200
@@ -3,17 +3,12 @@
         "~~/src/HOL/Library/LaTeXsugar"
 begin
 
-ML \<open>@{assert} true\<close>
-ML \<open>@{print} (2 + 3 +4)\<close>
-
+print_ML_antiquotations
 
-print_ML_antiquotations
-text \<open>
-Can we put an ML-val into the text?
+text \<open>Hallo ML Antiquotation:
+@{ML \<open>2 + 3\<close>}
+\<close>
 
-@{ML [display] \<open>2 + 3\<close>}
-
-\<close>
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
@@ -30,17 +25,16 @@
   HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
 
 ML_file "output_tutorial.ML"
-text \<open>
-Can we put an ML-val into the text?
-
-@{ML [gray] \<open>2 + 3\<close>}
-\<close>
-
 ML_file "antiquote_setup.ML"
 
 
 (*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *)
 setup {* AntiquoteSetup.setup *}
 
+print_ML_antiquotations
+
+text \<open>Hallo ML Antiquotation:
+@{ML \<open>2 + 3\<close> }
+\<close>
 
 end
\ No newline at end of file

--- a/ProgTutorial/First_Steps.thy	Tue May 14 13:39:31 2019 +0200
+++ b/ProgTutorial/First_Steps.thy	Tue May 14 16:59:53 2019 +0200
@@ -572,7 +572,7 @@
         |-> (fn x => fn y => x + y)*}
 
 text {* 
-  The combinator @{ML_ind ||>> in Basics} plays a central rôle whenever your
+  The combinator @{ML_ind ||>> in Basics} plays a central role whenever your
   task is to update a theory and the update also produces a side-result (for
   example a theorem). Functions for such tasks return a pair whose second
   component is the theory and the fist component is the side-result. Using

--- a/ProgTutorial/antiquote_setup.ML	Tue May 14 13:39:31 2019 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue May 14 16:59:53 2019 +0200
@@ -12,42 +12,52 @@
 fun prefix_lines prfx txt = 
   map (fn s => prfx ^ s) (split_lines txt)
 
-fun ml_with_vars ys txt = 
+fun ml_with_vars' ys txt = 
     implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]
 
-fun ml_with_struct (NONE) txt = txt 
-  | ml_with_struct (SOME st) txt = implode ["let open ", st, " in ", txt, " end"]
+fun ml_with_vars ys src = 
+    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 
+  | ml_with_struct (SOME st) src = 
+      ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source false src @ ML_Lex.read " end"
 
 fun ml_val vs stru txt = 
     txt |> ml_with_struct stru
-        |> ml_with_vars  vs 
+        |> ml_with_vars vs 
 
-fun ml_pat (lhs, pat) =
-  implode ["val ", translate_string (fn "\<dots>" => "_" | s => s) pat, " = ", lhs] 
+fun ml_pat pat lhs =
+  ML_Lex.read "val " @ ML_Lex.read (translate_string (fn "\<dots>" => "_" | s => s) pat) @ 
+  ML_Lex.read " = " @
+  ML_Lex.read_source false lhs 
 
-fun ml_struct txt = 
-  implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"]
+fun ml_struct src = 
+  ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @
+  ML_Lex.read_source false src @
+  ML_Lex.read " end"
 
-fun ml_type txt = 
-  implode ["val _ = NONE : (", txt, ") option"];
+fun ml_type src = 
+  ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option"
 
 (* eval function *)
-fun eval_fn ctxt exp =
-  ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags 
-    (Input.source false exp Position.no_range)
+fun eval_fn ctxt prep exp =
+  ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp)
 
 (* checks and prints a possibly open expressions, no index *)
-fun output_ml ctxt (txt, (vs, stru)) =
-  (eval_fn ctxt (ml_val vs stru txt); 
-   output ctxt (split_lines txt))
 
-val parser_ml = Scan.lift (Args.name --
+fun output_ml ctxt (src, (vs, stru)) =
+  (eval_fn ctxt (ml_val vs stru) src; 
+   output ctxt (split_lines (Input.source_content src)))
+ 
+val parser_ml = Scan.lift (Args.text_input --
   (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
    Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))) 
 
+
 (* checks and prints a single ML-item and produces an index entry *)
 fun output_ml_ind ctxt (txt, stru) =
-  (eval_fn ctxt (ml_val [] stru txt); 
+  (eval_fn ctxt (ml_val [] stru) (Input.string txt); 
    case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
      (NONE, _, "")  => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt)
    | (NONE, bn, qn)  => output_indexed ctxt {main = Code bn,  minor = Struct qn} (split_lines txt)
@@ -58,7 +68,7 @@
 
 (* checks and prints structures *)
 fun gen_output_struct outfn ctxt txt = 
-  (eval_fn ctxt (ml_struct txt); 
+  (eval_fn ctxt ml_struct (Input.string txt); 
    outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
 
 fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt 
@@ -73,37 +83,34 @@
 
 (* checks and prints types *)
 fun gen_output_type outfn ctxt txt = 
-  (eval_fn ctxt (ml_type txt); 
+  (eval_fn ctxt ml_type (Input.string txt); 
    outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
 
 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt
 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt 
 
-(* checks and expression agains a result pattern *)
+(* checks and expression against a result pattern *)
 fun output_response ctxt (lhs, pat) = 
-    (eval_fn ctxt (ml_pat (lhs, pat));
+    (eval_fn ctxt (ml_pat pat) lhs;
      (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*)
-     output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
+     output ctxt ((prefix_lines "" (Input.source_content lhs)) @ (prefix_lines "> " 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);
+    (eval_fn ctxt (ml_val [] NONE) lhs;
      (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *)
-     output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
+     output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " 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 lhs) @ (prefix_lines "> " pat)))
+    (output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat)))
 
 val single_arg = Scan.lift (Args.name)
-val two_args   = Scan.lift (Args.name -- Args.name)
+val two_args   = Scan.lift (Args.text_input -- Args.name)
 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"} parser_ml output_ml 
   #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind
   #> Thy_Output.antiquotation_raw @{binding "ML_type"} single_arg output_type
   #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind
@@ -115,19 +122,6 @@
   #> Thy_Output.antiquotation_raw @{binding "ML_response_fake"} two_args output_response_fake
   #> Thy_Output.antiquotation_raw @{binding "ML_response_fake_both"} two_args ouput_response_fake_both
 
-(* FIXME: experimental *)
-fun ml_eq (lhs, pat, eq) =
-  implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] 
-
-fun output_response_eq ctxt ((lhs, pat), eq) = 
-    (case eq of 
-       NONE => eval_fn ctxt (ml_pat (lhs, pat))
-     | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
-     output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
-
-val ml_response_setup = 
-  Thy_Output.antiquotation_raw @{binding "ML_response_eq"} test output_response_eq
-
 (* checks whether a file exists in the Isabelle distribution *)
 fun href_link txt =
 let 
@@ -188,9 +182,7 @@
 
 val setup =
   ml_setup #>
-  ml_response_setup #>
   ml_file_setup #>
   subgoals_setup #>
   raw_goal_state_setup
-
 end;