diff -r 126646f2aa88 -r 065f472c09ab CookBook/antiquote_setup.ML --- a/CookBook/antiquote_setup.ML Tue Dec 16 08:08:44 2008 +0000 +++ b/CookBook/antiquote_setup.ML Tue Dec 16 17:37:39 2008 +0100 @@ -22,9 +22,14 @@ fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; +val transform_cmts_str = + Source.of_string #> ML_Lex.source #> Source.exhaust #> + Chunks.transform_cmts #> implode; + fun output_ml ml src ctxt ((txt,ovars),pos) = (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); - ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) + txt |> transform_cmts_str |> space_explode "\n" |> + ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt) fun output_ml_aux ml src ctxt (txt,pos) = output_ml (K ml) src ctxt ((txt,()),pos)