diff -r dee4b3e66dfe -r 78aeca00bb54 CookBook/antiquote_setup.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/antiquote_setup.ML	Wed Oct 29 21:49:43 2008 +0100
@@ -0,0 +1,69 @@
+(* 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_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 txt = ml_val_open ([],[]) txt;
+
+fun ml_pat (rhs, pat) =
+  let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
+  in
+    "val " ^ pat' ^ " = " ^ rhs
+  end;
+
+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_ml_open ml src ctxt ((txt,ovars),pos) =
+  (ML_Context.eval_in (SOME ctxt) false pos (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,pos) =
+  output_ml_open (K ml) src ctxt ((txt,()),pos) 
+
+fun add_response_indicator txt =
+  map (fn s => "> " ^ 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)
+  in ThyOutput.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)
+  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.")
+
+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_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 (OuterParse.position Args.name)) (output_ml ml_val)),
+   ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
+      (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_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_struct)),
+   ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_type))];
+   
+end;