doc-src/rail.ML
changeset 38767 d8da44a8dd25
parent 37982 111ce9651564
child 42361 23f352990944
--- a/doc-src/rail.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/rail.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -97,8 +97,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{" "}}")), style)
   else ("Bad " ^ kind ^ " " ^ name, false)
   end;