--- a/ProgTutorial/output_tutorial.ML	Sun Aug 22 22:56:52 2010 +0800
+++ b/ProgTutorial/output_tutorial.ML	Sat Aug 28 13:27:16 2010 +0800
@@ -9,20 +9,20 @@
 val linenos = Unsynchronized.ref false
 
 
-fun output txt =
+fun output ctxt txt =
 let
   val prts = map Pretty.str txt
 in   
   prts
-  |> (if ! Thy_Output.quotes then map Pretty.quote else I)
-  |> (if ! Thy_Output.display then
-    map (Output.output o Pretty.string_of o Pretty.indent (! Thy_Output.indent))
+  |> (if Config.get ctxt Thy_Output.quotes then map Pretty.quote else I)
+  |> (if Config.get ctxt Thy_Output.display then
+    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Thy_Output.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 ! Thy_Output.break then Pretty.string_of else Pretty.str_of))
+    map (Output.output o (if Config.get ctxt Thy_Output.break then Pretty.string_of else Pretty.str_of))
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}")
 end
@@ -74,8 +74,8 @@
    Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"]
   | _ => "")
 
-fun output_indexed ind txt =
- txt |> output
+fun output_indexed ctxt ind txt =
+ txt |> output ctxt
      |> prefix (get_index ind)
      |> prefix (get_str_index ind)
 
@@ -84,8 +84,9 @@
   | boolean "false" = false
   | boolean s = error ("Bad boolean value: " ^ quote s);
 
-val _ = Thy_Output.add_options
- [("gray", Library.setmp_CRITICAL gray o boolean),
-  ("linenos", Library.setmp_CRITICAL linenos o boolean)]
+val _ = Thy_Output.add_option "gray" 
+  (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean)
+val _ = Thy_Output.add_option "linenos"  
+  (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean)
 
 end
\ No newline at end of file