diff -r b11653b11bd3 -r cd612b489504 CookBook/antiquote_setup_plus.ML
--- a/CookBook/antiquote_setup_plus.ML	Mon Oct 20 06:22:11 2008 +0000
+++ b/CookBook/antiquote_setup_plus.ML	Mon Oct 27 18:48:52 2008 +0100
@@ -1,79 +1,65 @@
-(*
-Auxiliary antiquotations for the Cookbook.
-
-*)
+(* Auxiliary antiquotations for the Cookbook. *)
 
 structure AntiquoteSetup: sig end =
 struct
 
 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
 
-fun ml_val ys txt = "fn " ^
-  (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^
-  " => (" ^ txt ^ ");";
+fun ml_val_open (ys, xs) txt = 
+  let fun ml_val_open_aux ys txt = 
+          "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
+  in
+    (case xs of
+       [] => ml_val_open_aux ys txt
+     | _  => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))
+  end;
 
-fun ml_val_open (ys, []) txt = ml_val ys txt
-  | ml_val_open (ys, xs) txt =
-      ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");
+fun ml_val txt = ml_val_open ([],[]) txt;
 
 fun ml_pat (rhs, pat) =
-  let val pat' = implode (map (fn "\\<dots>" => "_" | s => s)
-    (Symbol.explode pat))
+  let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
   in
     "val " ^ pat' ^ " = " ^ rhs
   end;
 
-(* modified from original *)
-fun ml_val txt = "fn _ => (" ^ txt ^ ");";
-fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;";
-fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
+fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
+fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
+fun ml_decl txt = txt
 
-fun output_verbatim f src ctxt x =
-  let val txt = f ctxt x
-  in
-    (if ! ThyOutput.source then str_of_source src else txt)
-    |> (if ! ThyOutput.quotes then quote else I)
-    |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt
-  end;
-
-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_open ml src ctxt (txt,ovars) =
+  (ML_Context.eval_in (SOME ctxt) false Position.none (ml ovars txt);
+  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))
 
 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)
+  output_ml_open (K ml) src ctxt (txt,()) 
 
 fun add_response_indicator txt =
-  space_implode "\n" (map (fn s => "> " ^ s) (space_explode "\n" txt))
+  map (fn s => "> " ^ s) (space_explode "\n" txt)
 
 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)
+  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 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)
+  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 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 --
+  [("ML_open", ThyOutput.args (Scan.lift (Args.name --
       (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
-       Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_old ml_val_open)),
+       Scan.optional (Args.parens (OuterParse.list1 Args.name)) []))) (output_ml_open ml_val_open)),
    ("ML_file", ThyOutput.args (Scan.lift Args.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) (output_ml ml_val)),
+   ("ML_decl", ThyOutput.args (Scan.lift Args.name) (output_ml ml_decl)),
    ("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)),