# HG changeset patch
# User wenzelm
# Date 1002643867 -7200
# Node ID bc0a84063a9c5382c4f8fe7667e003762e735f10
# Parent  883d559b0b8c2ecb881bd78392e5807c33f9bf5c
added global modes ref;

diff -r 883d559b0b8c -r bc0a84063a9c src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Mon Oct 08 15:23:20 2001 +0200
+++ b/src/Pure/Isar/isar_output.ML	Tue Oct 09 18:11:07 2001 +0200
@@ -17,6 +17,7 @@
     (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
   datatype markup = Markup | MarkupEnv | Verbatim
   val interest_level: int ref
+  val modes: string list ref
   val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) ->
     Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source ->
       (Toplevel.transition * (Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T
@@ -136,13 +137,15 @@
 
 (* eval_antiquote *)
 
+val modes = ref ([]: string list);
+
 fun eval_antiquote lex state (str, pos) =
   let
     fun expand (Antiquote.Text s) = s
       | expand (Antiquote.Antiq x) =
           let val (opts, src) = antiq_args lex x in
             options opts (fn () => command src state) ();  (*preview errors!*)
-            Library.setmp print_mode (Latex.modes @ ! print_mode)
+            Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
               (options opts (fn () => command src state)) ()
           end;
     val ants = Antiquote.antiquotes_of (str, pos);