diff -r 3d4b49921cdb -r c346c156a7cd CookBook/antiquote_setup.ML --- 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 "\\" => "_" | s => s) (Symbol.explode pat)) - in - "val " ^ pat' ^ " = " ^ rhs - end; + let + val pat' = implode (map (fn "\\" => "_" | 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) =