CookBook/antiquote_setup.ML
changeset 54 1783211b3494
parent 53 0c3580c831a4
child 57 065f472c09ab
--- a/CookBook/antiquote_setup.ML	Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/antiquote_setup.ML	Sat Dec 13 01:33:22 2008 +0000
@@ -43,6 +43,10 @@
   let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
   in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
 
+fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = 
+  let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
+  in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
+
 fun check_file_exists ctxt txt =
   if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
   else error ("Source file " ^ quote txt ^ " does not exist.")
@@ -60,6 +64,8 @@
       (output_ml_response ml_pat)),
    ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       (output_ml_response_fake ml_val)),
+   ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
+      (output_ml_response_fake_both ml_val)),
    ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)),
    ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))];