diff -r 0c3580c831a4 -r 1783211b3494 CookBook/antiquote_setup.ML --- 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))];