# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1234016493 0
# Node ID fe10da5354a3b978463245318ac701c4ea61bbb5
# Parent  5e309df5855798e9b2017ed6977477bd055bba31
further cleanup

diff -r 5e309df58557 -r fe10da5354a3 CookBook/antiquote_setup.ML
--- a/CookBook/antiquote_setup.ML	Sat Feb 07 12:05:02 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Sat Feb 07 14:21:33 2009 +0000
@@ -35,23 +35,28 @@
 fun output_ml_aux ml src ctxt (txt,pos) =
   output_ml (K ml) src ctxt ((txt,()),pos) 
 
-fun add_response_indicator txt =
-  map (fn s => "> " ^ s) (space_explode "\n" txt)
+fun string_explode str txt =
+  map (fn s => str ^ s) (space_explode "\n" txt)
 
 fun output_ml_response ml src ctxt ((lhs,pat),pos) = 
   (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat));
   let 
-      val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
+      val txt = (string_explode "" lhs) @ (string_explode "> " pat)
   in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
 
 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = 
   (ML_Context.eval_in (SOME ctxt) false pos (ml lhs);
-  let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
+  let val txt = (string_explode "" lhs) @ (string_explode "> " pat)
   in Chunks.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 Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
+fun output_ml_response_fake_both src node =
+let 
+  fun ouput src ctxt (lhs,pat) = 
+    Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt 
+     ((string_explode "" lhs) @ (string_explode "> " pat))
+in
+  ThyOutput.args (Scan.lift (Args.name -- Args.name)) ouput src node
+end
 
 fun check_file_exists src node =
 let 
@@ -100,8 +105,7 @@
       (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_response_fake_both", output_ml_response_fake_both),
    ("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)),
    ("subgoals", output_goals)];
diff -r 5e309df58557 -r fe10da5354a3 cookbook.pdf
Binary file cookbook.pdf has changed