# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1233248919 0
# Node ID b071a0b88298cdd758dd0abaf2d074e44dd8beaa
# Parent  fee4942c4770d8765d8f33e826592c158d5898ba
made chunks aware of the gray-option

diff -r fee4942c4770 -r b071a0b88298 CookBook/antiquote_setup.ML
--- a/CookBook/antiquote_setup.ML	Thu Jan 29 09:46:36 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Thu Jan 29 17:08:39 2009 +0000
@@ -3,34 +3,6 @@
 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))
-    #> 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 = 
@@ -58,7 +30,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" |>
-   output_list (fn _ => fn s => Pretty.str s) src ctxt)
+   Chunks.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) 
@@ -70,16 +42,16 @@
   (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat));
   let 
       val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
-  in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+  in Chunks.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 output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+  in Chunks.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 output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
+  in Chunks.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 ()
diff -r fee4942c4770 -r b071a0b88298 CookBook/chunks.ML
--- 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