CookBook/antiquote_setup.ML
changeset 51 c346c156a7cd
parent 49 a0edabf14457
child 53 0c3580c831a4
--- 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) =