--- a/ProgTutorial/chunks.ML	Fri May 29 12:15:48 2009 +0200
+++ b/ProgTutorial/chunks.ML	Sat May 30 11:12:46 2009 +0200
@@ -2,39 +2,6 @@
 structure Chunks =
 struct
 
-(* rebuilding the output function from ThyOutput in order to *)
-(* enable the options [gray, linenos]                        *)
-
-val gray = ref false;
-val linenos = ref false
-
-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))
-    #> space_implode "\\isasep\\isanewline%\n"
-    #> (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
-    map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
-    #> space_implode "\\isasep\\isanewline%\n"
-    #> enclose "\\isa{" "}");
-
-
-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),
-  ("linenos", Library.setmp linenos o boolean)]
-
-
-
-
 (** theory data **)
 
 structure ChunkData = TheoryDataFun
@@ -158,8 +125,7 @@
           end)
     val txt = spc ^ implode (transform_cmts toks')
   in
-    txt |> split_lines |>
-    (map Pretty.str) |> output 
+    txt |> split_lines |> OutputFN.output 
   end;
 
 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;