CookBook/antiquote_setup.ML
changeset 57 065f472c09ab
parent 54 1783211b3494
child 72 7b8c4fe235aa
--- 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)