doc-src/antiquote_setup.ML

--- a/doc-src/antiquote_setup.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/antiquote_setup.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -71,8 +71,8 @@
     in
       "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
       (txt'
-      |> (if ! Thy_Output.quotes then quote else I)
-      |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+      |> (if Config.get ctxt Thy_Output.quotes then quote else I)
+      |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
           else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
     end);
 
@@ -93,18 +93,18 @@
   (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
   (fn {context = ctxt, ...} =>
     map (apfst (Thy_Output.pretty_thm ctxt))
-    #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I)
-    #> (if ! Thy_Output.display
+    #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
+    #> (if Config.get ctxt Thy_Output.display
         then
           map (fn (p, name) =>
-            Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^
-            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
+            Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
+            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
           #> space_implode "\\par\\smallskip%\n"
           #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
         else
           map (fn (p, name) =>
             Output.output (Pretty.str_of p) ^
-            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
+            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
           #> space_implode "\\par\\smallskip%\n"
           #> enclose "\\isa{" "}"));
 
@@ -112,7 +112,8 @@
 (* theory file *)
 
 val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
-  (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name]));
+  (fn {context = ctxt, ...} =>
+    fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
 
 
 (* Isabelle/Isar entities (with index) *)
@@ -152,8 +153,9 @@
           idx ^
           (Output.output name
             |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
-            |> (if ! Thy_Output.quotes then quote else I)
-            |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+            |> (if Config.get ctxt Thy_Output.quotes then quote else I)
+            |> (if Config.get ctxt Thy_Output.display
+                then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
                 else hyper o enclose "\\mbox{\\isa{" "}}"))
         else error ("Bad " ^ kind ^ " " ^ quote name)
       end);