--- a/CookBook/antiquote_setup.ML Tue Nov 25 05:19:27 2008 +0000
+++ b/CookBook/antiquote_setup.ML Fri Nov 28 05:19:55 2008 +0100
@@ -3,8 +3,6 @@
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 ^ ")";
@@ -17,10 +15,9 @@
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;
+ 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";
@@ -37,7 +34,8 @@
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)
+ 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) =