--- 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))];