--- a/ProgTutorial/Recipes/Antiquotes.thy	Tue May 21 16:22:30 2019 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Wed May 22 12:38:51 2019 +0200
@@ -46,12 +46,14 @@
 
 fun output_ml ctxt code_txt =
 let
-  val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt)
+  val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags 
+    (Input.pos_of code_txt) (ml_val code_txt)
 in 
    Pretty.str (fst (Input.source_content code_txt))
 end
 
-val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close>
+val ml_checked_setup = Thy_Output.antiquotation_pretty_source 
+  @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close>
 
 setup \<open>ml_checked_setup\<close>
 
@@ -80,25 +82,7 @@
   information about the line number, in case an error is detected. We 
   can improve the code above slightly by writing 
 \<close>
-(* FIXME: remove
-ML%linenosgray{*fun output_ml ctxt (code_txt, pos) =
-let
-  val srcpos = {delimited = false, pos = pos, text = ml_val code_txt}
-in
-  (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos;
-   code_txt 
-   |> space_explode "\n"
-   |> map Pretty.str
-   |> Pretty.list "" ""
-   |> Document_Antiquotation.output ctxt
-   |> Latex.string)
-end
 
-val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"}
-         (Scan.lift (Parse.position Args.name)) output_ml *}
-
-setup {* ml_checked_setup2 *}
-*)
 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 
@@ -129,16 +113,11 @@
 \<close>
 
 ML%linenosgray\<open>fun ml_pat pat code =
-  ML_Lex.read "val" @ ML_Lex.read_source pat @ ML_Lex.read " = " @ ML_Lex.read_source code\<close>
+  ML_Lex.read "val" @ 
+  ML_Lex.read_source pat @ 
+  ML_Lex.read " = " @ 
+  ML_Lex.read_source code\<close>
 
-(*
-ML %grayML{*fun ml_pat code_txt pat =
-let val pat' = 
-         implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
-in 
-  ml_enclose ("val " ^ pat' ^ " = ") "" code_txt 
-end*}
-*)
 text \<open>
   Next we add a response indicator to the result using:
 \<close>
@@ -153,36 +132,21 @@
 ML %linenosgray\<open>
 fun output_ml_resp ctxt (code_txt, pat) =
 let
-  val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_pat pat code_txt)
+  val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags 
+    (Input.pos_of code_txt) (ml_pat pat code_txt)
   val code = space_explode "\n" (fst (Input.source_content code_txt))
   val resp = add_resp (space_explode "\n" (fst (Input.source_content pat)))
 in 
    Pretty.str (cat_lines (code @ resp))
 end
 
-val ml_response_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_resp"} (Scan.lift (Args.text_input -- Args.text_input)) output_ml_resp
+val ml_response_setup = Thy_Output.antiquotation_pretty_source 
+  @{binding "ML_resp"} 
+  (Scan.lift (Args.text_input -- Args.text_input)) 
+  output_ml_resp
 
 \<close>
 
-(*
-ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = 
-  (let
-     val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos}
-   in
-     ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos 
-   end;
-   let 
-     val code_output = space_explode "\n" code_txt 
-     val resp_output = add_resp (space_explode "\n" pat)
-   in 
-     Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) 
-   end)
-
-
-val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} 
-          (Scan.lift (Parse.position (Args.text_input -- Args.text_input))) 
-             output_ml_resp*}
-*)
 setup \<open>ml_response_setup\<close>
 
 (* FIXME *)