--- a/ProgTutorial/output_tutorial.ML	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/output_tutorial.ML	Tue May 14 11:10:53 2019 +0200
@@ -5,28 +5,29 @@
 (* rebuilding the output function from Thy_Output in order to *)
 (* enable the options [gray, linenos]                        *)
 
-val gray = Unsynchronized.ref false
-val linenos = Unsynchronized.ref false
+val thy_output_linenos = Attrib.setup_config_bool @{binding linenos} (K false)
+val thy_output_gray = Attrib.setup_config_bool @{binding gray} (K false)
 
-
-fun output ctxt txt =
+fun output_raw ctxt txt =
 let
   val prts = map Pretty.str txt
 in   
   prts
-  |> (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))
+  |> (if Config.get ctxt Document_Antiquotation.thy_output_quotes then map Pretty.quote else I)
+  |> (if Config.get ctxt Document_Antiquotation.thy_output_display then
+    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Document_Antiquotation.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) 
+    #> (if Config.get ctxt thy_output_linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 
+    #> (if  Config.get ctxt thy_output_gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   else
-    map (Output.output o (if Config.get ctxt Thy_Output.break then Pretty.string_of else Pretty.str_of))
+    map (Output.output o (if Config.get ctxt Document_Antiquotation.thy_output_break then Pretty.string_of else Pretty.unformatted_string_of))
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}")
 end
 
+fun output ctxt txt = Latex.string (output_raw ctxt txt)
+
 datatype indstring =
   NoString
 | Plain   of string
@@ -75,22 +76,19 @@
   | _ => "")
 
 fun output_indexed ctxt ind txt =
- txt |> output ctxt
+ txt |> output_raw ctxt
      |> prefix (get_index ind)
      |> prefix (get_str_index ind)
+     |> Latex.string
 
 fun boolean "" = true
   | boolean "true" = true
   | boolean "false" = false
   | boolean s = error ("Bad boolean value: " ^ quote s);
 
-val gray_setup = Thy_Output.add_option @{binding "gray"} 
-  (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean)
-val linenos_setup = Thy_Output.add_option @{binding "linenos"}  
-  (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean)
+val _ = Theory.setup 
+  (Document_Antiquotation.setup_option @{binding gray} (Config.put thy_output_gray o boolean) #> 
+   Document_Antiquotation.setup_option @{binding linenos} (Config.put thy_output_linenos o boolean) ); 
 
-val setup =
-  gray_setup #>
-  linenos_setup 
 
 end
\ No newline at end of file