--- a/CookBook/antiquote_setup_plus.ML	Fri Oct 10 17:06:26 2008 +0200
+++ b/CookBook/antiquote_setup_plus.ML	Fri Oct 10 17:07:52 2008 +0200
@@ -3,14 +3,74 @@
 
 *)
 
-local structure O = ThyOutput
-in
-  fun check_exists f = 
-    if File.exists (Path.explode ("~~/src/" ^ f)) then ()
-    else error ("Source file " ^ quote f ^ " does not exist.")
-  
-  val _ = O.add_commands
-   [("ML_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
-         (check_exists name; Pretty.str name))))];
+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, []) txt = ml_val ys txt
+  | ml_val_open (ys, xs) txt =
+      ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");
+
+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")
+  end;
+
+fun output_ml 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));
 
-end
\ No newline at end of file
+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)))));
+
+fun check_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))),
+   ("ML_file", ThyOutput.args (Scan.lift Args.name)
+      (ThyOutput.output (fn _ => fn name => (check_exists name; Pretty.str name))))];
+
+end;