diff -r 90bee31628dc -r 18f90044c777 CookBook/chunks.ML
--- a/CookBook/chunks.ML	Thu Mar 12 08:11:02 2009 +0100
+++ b/CookBook/chunks.ML	Thu Mar 12 14:25:35 2009 +0000
@@ -2,20 +2,14 @@
 structure Chunks =
 struct
 
-(* rebuilding the output_list function from ThyOutput in order to *)
-(* enable the options [gray, linenos] *)
+(* rebuilding the output function from ThyOutput in order to *)
+(* enable the options [gray, linenos]                        *)
 
 val gray = ref false;
 val linenos = ref false
 
-fun boolean "" = true
-  | boolean "true" = true
-  | boolean "false" = false
-  | boolean s = error ("Bad boolean value: " ^ quote s);
-
-fun output_list pretty src ctxt xs =
-  map (pretty ctxt) xs        (*always pretty in order to exhibit errors!*)
-  |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I)
+fun output prts =
+  prts
   |> (if ! ThyOutput.quotes then map Pretty.quote else I)
   |> (if ! ThyOutput.display then
     map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
@@ -23,12 +17,16 @@
     #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 
     #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- else
+  else
     map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}");
 
-fun output pretty src ctxt = output_list pretty src ctxt o single
+
+fun boolean "" = true
+  | boolean "true" = true
+  | boolean "false" = false
+  | boolean s = error ("Bad boolean value: " ^ quote s);
 
 val _ = ThyOutput.add_options
  [("gray", Library.setmp gray o boolean),
@@ -161,7 +159,7 @@
     val txt = spc ^ implode (transform_cmts toks')
   in
     txt |> split_lines |>
-    output_list (fn _ => fn s => Pretty.str s) src ctxt
+    (map Pretty.str) |> output 
   end;
 
 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;