diff -r 35e1dff0d9bb -r b11653b11bd3 CookBook/antiquote_setup_plus.ML
--- a/CookBook/antiquote_setup_plus.ML	Fri Oct 17 17:41:34 2008 -0400
+++ b/CookBook/antiquote_setup_plus.ML	Mon Oct 20 06:22:11 2008 +0000
@@ -36,41 +36,48 @@
     |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt
   end;
 
-fun output_ml ml = output_verbatim
+fun output_ml_old ml = output_verbatim
   (fn ctxt => fn ((txt, p), pos) =>
      (ML_Context.eval_in (SOME ctxt) false pos (ml p txt);
       txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |>
       Chunks.transform_cmts |> implode));
 
-fun output_ml_response ml = output_verbatim
-  (fn ctxt => fn ((x as (rhs, pat), p), pos) =>
-     (ML_Context.eval_in (SOME ctxt) false pos (ml p x);
-      rhs ^ "\n" ^
-      space_implode "\n" (map (fn s => "> " ^ s)
-        (space_explode "\n" pat))));
+fun output_ml ml src ctxt txt =
+  (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt);
+  ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt)
+
+fun add_response_indicator txt =
+  space_implode "\n" (map (fn s => "> " ^ s) (space_explode "\n" txt))
 
-fun output_ml_checked ml src ctxt (txt, pos) =
- (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
- (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
-  |> (if ! ThyOutput.quotes then quote else I)
-  |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt)
+fun output_ml_response ml src ctxt (lhs,pat) = 
+  (ML_Context.eval_in (SOME ctxt) false Position.none (ml (lhs,pat));
+  let val txt = lhs ^ "\n" ^ (add_response_indicator pat)
+  in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end)
+
+fun output_ml_response_fake ml src ctxt (lhs,pat) = 
+  (ML_Context.eval_in (SOME ctxt) false Position.none (ml lhs);
+  let val txt = lhs ^ "\n" ^ (add_response_indicator pat)
+  in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end)
 
 fun check_file_exists ctxt name =
   if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then ()
   else error ("Source file " ^ quote name ^ " does not exist.")
 
+
+
 val _ = ThyOutput.add_commands
   [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
       (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
-       Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml ml_val_open)),
-   ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position
-        ((Args.name -- Args.name) >> rpair ()))) (output_ml_response (K ml_pat))),
+       Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_old ml_val_open)),
    ("ML_file", ThyOutput.args (Scan.lift Args.name)
-      (ThyOutput.output (fn _ => fn name => (check_file_exists name; Pretty.str name)))),
+      (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))),
    ("ML_text", ThyOutput.args (Scan.lift Args.name)
       (ThyOutput.output (fn _ => fn s => Pretty.str s))),
-   ("ML", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_val)),
-   ("ML_struct", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_struct)),
-   ("ML_type", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_type))];
+   ("ML", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val)),
+   ("ML_response", ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response ml_pat)),
+   ("ML_response_fake", 
+           ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response_fake ml_val)),
+   ("ML_struct", ThyOutput.args (Scan.lift Args.name) (output_ml ml_struct)),
+   ("ML_type", ThyOutput.args (Scan.lift Args.name) (output_ml ml_type))];
    
 end;