--- a/ProgTutorial/antiquote_setup.ML	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Thu May 16 19:56:12 2019 +0200
@@ -45,6 +45,21 @@
 fun eval_fn ctxt prep exp =
   ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp)
 
+(* Evalate expression and convert result to a string *)
+fun eval_response ctxt exp =
+let 
+  fun compute exp = 
+     let 
+       val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source false 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 ""
+     end 
+in
+  (compute exp 
+   handle ERROR s => s)
+end
+
 (* checks and prints a possibly open expressions, no index *)
 
 fun output_ml ctxt (src, (vs, stru)) =
@@ -55,37 +70,60 @@
   (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
    Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))) 
 
+fun output_ml_response ctxt src =
+let 
+  val res = eval_response ctxt src
+in 
+  OutputTutorial.output ctxt ([Input.source_content src] @ [Library.prefix_lines "> " res])
+end
+
 
 (* 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) (Input.string txt); 
+fun output_ml_ind ctxt (src, stru) =
+let 
+  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
      (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)
    | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt))
+end
 
-val parser_ml_ind = Scan.lift (Args.name --
+val parser_ml_ind = Scan.lift (Args.text_input --
   Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))
 
 (* checks and prints structures *)
-fun gen_output_struct outfn ctxt txt = 
-  (eval_fn ctxt ml_struct (Input.string txt); 
+fun gen_output_struct outfn ctxt src = 
+let 
+  val txt = Input.source_content src
+in
+  (eval_fn ctxt ml_struct src; 
    outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
+end
 
 fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt 
 fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt 
 
 (* prints functors; no checks *)
-fun gen_output_funct outfn txt = 
+fun gen_output_funct outfn src = 
+let
+  val txt = Input.source_content src
+in
   (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
+end
 
 fun output_funct ctxt = gen_output_funct (K (output ctxt)) 
 fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt)
 
 (* checks and prints types *)
-fun gen_output_type outfn ctxt txt = 
-  (eval_fn ctxt ml_type (Input.string txt); 
+fun gen_output_type outfn ctxt src = 
+let 
+  val txt = Input.source_content src
+in
+  (eval_fn ctxt ml_type src; 
    outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
+end
 
 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt
 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt 
@@ -109,22 +147,20 @@
     (output ctxt ((split_lines (Input.source_content lhs)) @ 
      (prefix_lines "> " (dots_pat (Input.source_content pat)))))
 
-val single_arg = Scan.lift (Args.name)
+val single_arg = Scan.lift (Args.text_input)
 val two_args   = Scan.lift (Args.text_input -- 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"} parser_ml output_ml
+  #> Thy_Output.antiquotation_raw @{binding "ML_response"} single_arg output_ml_response
   #> 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
-  #> Thy_Output.antiquotation_raw @{binding "ML_struct"} single_arg output_struct
-  #> Thy_Output.antiquotation_raw @{binding "ML_struct_ind"} single_arg output_struct_ind
-  #> Thy_Output.antiquotation_raw @{binding "ML_funct"} single_arg output_funct
-  #> Thy_Output.antiquotation_raw @{binding "ML_funct_ind"} single_arg output_funct_ind
-  #> Thy_Output.antiquotation_raw @{binding "ML_response"} two_args output_response
-  #> 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
+  #> Thy_Output.antiquotation_raw @{binding "ML_structure_ind"} single_arg output_struct_ind
+  #> Thy_Output.antiquotation_raw @{binding "ML_functor_ind"} single_arg output_funct_ind
+  #> Thy_Output.antiquotation_raw @{binding "ML_matchresult"} two_args output_response
+  #> Thy_Output.antiquotation_raw @{binding "ML_matchresult_fake"} two_args output_response_fake
+  #> Thy_Output.antiquotation_raw @{binding "ML_matchresult_fake_both"} two_args ouput_response_fake_both
 
 (* checks whether a file exists in the Isabelle distribution *)
 fun href_link txt =
@@ -135,10 +171,14 @@
  implode [raw "\\href{", raw path, raw txt, raw "}{", get_word txt, raw "}"]
 end 
 
-fun check_file_exists _ txt =
+fun check_file_exists _ src =
+let
+  val txt = Input.source_content src
+in
   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
    then Latex.string (href_link txt)
    else error (implode ["Source file ", quote txt, " does not exist."]))
+end
 
 val ml_file_setup = Thy_Output.antiquotation_raw @{binding "ML_file"} single_arg check_file_exists