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