--- a/CookBook/antiquote_setup.ML	Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Wed Jan 14 23:44:14 2009 +0000
@@ -3,6 +3,36 @@
 structure AntiquoteSetup: sig end =
 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))*)
+    map (Output.output o Pretty.str_of)
+    #> space_implode "\\isasep\\isanewline%\n"
+    #> enclose "\\isa{" "}");
+
+val _ = ThyOutput.add_options
+ [("gray", Library.setmp gray o boolean)]
+
+
+(* main body *)
 fun ml_val_open (ys, xs) txt = 
   let fun ml_val_open_aux ys txt = 
           "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
@@ -29,7 +59,7 @@
 fun output_ml ml src ctxt ((txt,ovars),pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt);
    txt |> transform_cmts_str |> space_explode "\n" |>
-   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt)
+   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) 
@@ -41,16 +71,16 @@
   (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat));
   let 
       val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
-  in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+  in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
 
 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = 
   (ML_Context.eval_in (SOME ctxt) false pos (ml lhs);
   let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
-  in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+  in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
 
 fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = 
   let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
-  in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
+  in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
 
 fun check_file_exists ctxt txt =
   if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()