--- 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)