PrintMode.with_modes;

--- a/src/Pure/Isar/isar_cmd.ML	Mon Jul 23 16:45:02 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Jul 23 16:45:03 2007 +0200
@@ -331,15 +331,12 @@
 
 (* print state *)
 
-fun with_modes modes e =
-  Library.setmp print_mode (modes @ ! print_mode) e ();
-
 fun set_limit _ NONE = ()
   | set_limit r (SOME n) = r := n;
 
 fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
   (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
-    with_modes modes (fn () => Toplevel.print_state true state)));
+    PrintMode.with_modes modes (Toplevel.print_state true) state));
 
 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
@@ -586,8 +583,9 @@
     val T = ProofContext.read_typ ctxt s;
   in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end;
 
-fun print_item string_of (modes, arg) = Toplevel.keep (fn state => with_modes modes (fn () =>
-  writeln (string_of (Toplevel.enter_proof_body state) arg)));
+fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
+  PrintMode.with_modes modes (fn () =>
+    writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
 
 in
 

--- a/src/Pure/ProofGeneral/pgml_isabelle.ML	Mon Jul 23 16:45:02 2007 +0200
+++ b/src/Pure/ProofGeneral/pgml_isabelle.ML	Mon Jul 23 16:45:03 2007 +0200
@@ -16,7 +16,7 @@
 (** print mode **)
 
 val pgmlN = "PGML";
-fun pgml_mode f x = setmp print_mode (pgmlN :: ! print_mode) f x;
+fun pgml_mode f x = PrintMode.with_modes [pgmlN] f x;
 
 val _ = Markup.add_mode pgmlN (fn markup as (name, _) => ("", ""));
 

--- a/src/Pure/Thy/html.ML	Mon Jul 23 16:45:02 2007 +0200
+++ b/src/Pure/Thy/html.ML	Mon Jul 23 16:45:03 2007 +0200
@@ -51,7 +51,7 @@
 (* mode *)
 
 val htmlN = "HTML";
-fun html_mode f x = setmp print_mode (htmlN :: ! print_mode) f x;
+fun html_mode f x = PrintMode.with_modes [htmlN] f x;
 
 
 (* symbol output *)

--- a/src/Pure/Thy/thy_output.ML	Mon Jul 23 16:45:02 2007 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Jul 23 16:45:03 2007 +0200
@@ -146,7 +146,7 @@
       | expand (Antiquote.Antiq x) =
           let val (opts, src) = Antiquote.scan_arguments lex antiq x in
             options opts (fn () => command src node) ();  (*preview errors!*)
-            Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
+            PrintMode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings (options opts (fn () => command src node))) ()
           end;
     val ants = Antiquote.scan_antiquotes (str, pos);
@@ -413,7 +413,7 @@
   ("display", Library.setmp display o boolean),
   ("break", Library.setmp break o boolean),
   ("quotes", Library.setmp quotes o boolean),
-  ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
+  ("mode", fn s => fn f => PrintMode.with_modes [s] f),
   ("margin", Pretty.setmp_margin o integer),
   ("indent", Library.setmp indent o integer),
   ("source", Library.setmp source o boolean),