# HG changeset patch
# User wenzelm
# Date 1190039803 -7200
# Node ID bc889c3d55a3d19344aaa446f5a2b1750f7827f5
# Parent  d1b315bdb8d77bb779244cd89edb9b39dfda30ee
added print_mode_value (CRITICAL);

diff -r d1b315bdb8d7 -r bc889c3d55a3 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Mon Sep 17 16:36:41 2007 +0200
+++ b/src/Pure/General/print_mode.ML	Mon Sep 17 16:36:43 2007 +0200
@@ -9,6 +9,7 @@
 signature BASIC_PRINT_MODE =
 sig
   val print_mode: string list ref
+  val print_mode_value: unit -> string list
   val print_mode_active: string -> bool
 end;
 
@@ -23,7 +24,9 @@
 struct
 
 val print_mode = ref ([]: string list);
-fun print_mode_active s = member (op =) (! print_mode) s;
+
+fun print_mode_value () = NAMED_CRITICAL "print_mode" (fn () => ! print_mode);
+fun print_mode_active s = member (op =) (print_mode_value ()) s;
 
 fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
   setmp print_mode (modes @ ! print_mode) f x);
diff -r d1b315bdb8d7 -r bc889c3d55a3 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Sep 17 16:36:41 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Sep 17 16:36:43 2007 +0200
@@ -567,7 +567,7 @@
     val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
   in
     Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
-      (lookup_tokentr tokentrtab (! print_mode))
+      (lookup_tokentr tokentrtab (print_mode_value ()))
       (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
   end;
 
diff -r d1b315bdb8d7 -r bc889c3d55a3 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Mon Sep 17 16:36:41 2007 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Mon Sep 17 16:36:43 2007 +0200
@@ -172,15 +172,15 @@
 val no_bracketsN = "no_brackets";
 
 fun no_brackets () =
-  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) (! print_mode)
-    = SOME no_bracketsN;
+  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
+    (print_mode_value ()) = SOME no_bracketsN;
 
 val type_bracketsN = "type_brackets";
 val no_type_bracketsN = "no_type_brackets";
 
 fun no_type_brackets () =
-  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) (! print_mode)
-    <> SOME type_bracketsN;
+  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
+    (print_mode_value ()) <> SOME type_bracketsN;
 
 
 (* parse ast translations *)