diff -r cd612b489504 -r 02f76f1b6e7b CookBook/antiquote_setup_plus.ML
--- a/CookBook/antiquote_setup_plus.ML	Mon Oct 27 18:48:52 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* 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) =
-  (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 =
-  output_ml_open (K ml) src ctxt (txt,()) 
-
-fun add_response_indicator 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 = (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 = (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 (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 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)),
-   ("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;