--- a/CookBook/antiquote_setup_plus.ML	Tue Oct 14 01:33:55 2008 -0400
+++ b/CookBook/antiquote_setup_plus.ML	Fri Oct 17 05:02:04 2008 -0400
@@ -16,16 +16,24 @@
   | ml_val_open (ys, xs) txt =
       ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");
 
+fun ml_pat (rhs, 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 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)
-    |> (if ! ThyOutput.display then enclose "\\begin{alltt}\n" "\n\\end{alltt}"
-    else
-      split_lines
-      #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
-      #> space_implode "\\isasep\\\\%\n")
+    |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt
   end;
 
 fun output_ml ml = output_verbatim
@@ -34,32 +42,20 @@
       txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |>
       Chunks.transform_cmts |> implode));
 
-fun transform_char "\\" = "{\\isacharbackslash}"
-  | transform_char "$" = "{\\$}"
-  | transform_char "{" = "{\\isacharbraceleft}"
-  | transform_char "}" = "{\\isacharbraceright}"
-  | transform_char x = x;
-
-fun transform_symbol x =
-  if Symbol.is_char x then transform_char x else Latex.output_symbols [x];
-
-fun transform_str s = implode (map transform_symbol (Symbol.explode s));
-
-fun ml_pat (rhs, pat) =
-  let val pat' = implode (map (fn "\\<dots>" => "_" | s => s)
-    (Symbol.explode pat))
-  in
-    "val " ^ pat' ^ " = " ^ rhs
-  end;
-
 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);
-      transform_str rhs ^ "\n\n" ^
-      space_implode "\n" (map (enclose "\\textit{" "}")
-        (space_explode "\n" (transform_str pat)))));
+      rhs ^ "\n" ^
+      space_implode "\n" (map (fn s => "> " ^ s)
+        (space_explode "\n" pat))));
 
-fun check_exists ctxt name =
+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 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.")
 
@@ -68,9 +64,13 @@
       (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))),
+        ((Args.name -- Args.name) >> rpair ()))) (output_ml_response (K ml_pat))),
    ("ML_file", ThyOutput.args (Scan.lift Args.name)
-      (ThyOutput.output (fn _ => fn name => (check_exists name; Pretty.str name))))];
-
+      (ThyOutput.output (fn _ => fn name => (check_file_exists name; Pretty.str name)))),
+   ("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))];
+   
 end;