--- a/CookBook/chunks.ML	Thu Jan 29 09:46:36 2009 +0000
+++ b/CookBook/chunks.ML	Thu Jan 29 17:08:39 2009 +0000
@@ -1,6 +1,34 @@
+
 structure Chunks =
 struct
 
+(* rebuilding the output_list function from ThyOutput in order to *)
+(* enable the option [gray] *)
+
+val gray = 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)
+  |> (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))
+    #> space_implode "\\isasep\\isanewline%\n"
+    #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
+    #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ else
+    map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
+    #> space_implode "\\isasep\\isanewline%\n"
+    #> enclose "\\isa{" "}");
+
+val _ = ThyOutput.add_options
+ [("gray", Library.setmp gray o boolean)]
+
 (** theory data **)
 
 structure ChunkData = TheoryDataFun
@@ -125,7 +153,7 @@
     val txt = spc ^ implode (transform_cmts toks')
   in
     txt |> split_lines |>
-    ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt
+    output_list (fn _ => fn s => Pretty.str s) src ctxt
   end;
 
 val _ = ThyOutput.add_commands