# HG changeset patch
# User berghofe
# Date 1229445459 -3600
# Node ID 065f472c09ab244d3187f833b778d11c0d69b50f
# Parent  126646f2aa88f1de1b6db471089f2f50e6c57015
Repaired output of marginal comments in ML antiquotation.

diff -r 126646f2aa88 -r 065f472c09ab CookBook/Base.thy
--- a/CookBook/Base.thy	Tue Dec 16 08:08:44 2008 +0000
+++ b/CookBook/Base.thy	Tue Dec 16 17:37:39 2008 +0100
@@ -1,8 +1,8 @@
 theory Base
 imports Main
 uses
+  "chunks.ML"
   "antiquote_setup.ML"
-  "chunks.ML"
 begin
 
 end
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) 
diff -r 126646f2aa88 -r 065f472c09ab CookBook/chunks.ML
--- a/CookBook/chunks.ML	Tue Dec 16 08:08:44 2008 +0000
+++ b/CookBook/chunks.ML	Tue Dec 16 17:37:39 2008 +0100
@@ -99,7 +99,7 @@
            Scan.repeat (Scan.unless (Scan.this_string "}*)")
              (Scan.one (not o Symbol.is_eof))) --|
            Scan.this_string "}*)" >>
-           (enclose "\\hfill\\textrm{\\textit{" "}}" o implode))
+           (Symbol.encode_raw o enclose "\\hfill\\textrm{\\textit{" "}}" o implode))
      || Scan.one not_eof >> ML_Lex.content_of)) #>
   fst;
 
@@ -124,10 +124,8 @@
           end)
     val txt = spc ^ implode (transform_cmts toks')
   in
-    ((if ! ThyOutput.source then str_of_source src else txt)
-    |> (if ! ThyOutput.quotes then quote else I)
-    |> (if ! ThyOutput.display then enclose "\\begin{alltt}\n" "\n\\end{alltt}"
-        else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
+    txt |> split_lines |>
+    ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt
   end;
 
 val _ = ThyOutput.add_commands
diff -r 126646f2aa88 -r 065f472c09ab cookbook.pdf
Binary file cookbook.pdf has changed