1.1 --- a/src/Pure/General/print_mode.ML	Mon Sep 17 16:36:41 2007 +0200
     1.2 +++ b/src/Pure/General/print_mode.ML	Mon Sep 17 16:36:43 2007 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  signature BASIC_PRINT_MODE =
     1.5  sig
     1.6    val print_mode: string list ref
     1.7 +  val print_mode_value: unit -> string list
     1.8    val print_mode_active: string -> bool
     1.9  end;
    1.10  
    1.11 @@ -23,7 +24,9 @@
    1.12  struct
    1.13  
    1.14  val print_mode = ref ([]: string list);
    1.15 -fun print_mode_active s = member (op =) (! print_mode) s;
    1.16 +
    1.17 +fun print_mode_value () = NAMED_CRITICAL "print_mode" (fn () => ! print_mode);
    1.18 +fun print_mode_active s = member (op =) (print_mode_value ()) s;
    1.19  
    1.20  fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
    1.21    setmp print_mode (modes @ ! print_mode) f x);

     2.1 --- a/src/Pure/Syntax/syntax.ML	Mon Sep 17 16:36:41 2007 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Sep 17 16:36:43 2007 +0200
     2.3 @@ -567,7 +567,7 @@
     2.4      val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
     2.5    in
     2.6      Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
     2.7 -      (lookup_tokentr tokentrtab (! print_mode))
     2.8 +      (lookup_tokentr tokentrtab (print_mode_value ()))
     2.9        (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
    2.10    end;
    2.11  

     3.1 --- a/src/Pure/Syntax/type_ext.ML	Mon Sep 17 16:36:41 2007 +0200
     3.2 +++ b/src/Pure/Syntax/type_ext.ML	Mon Sep 17 16:36:43 2007 +0200
     3.3 @@ -172,15 +172,15 @@
     3.4  val no_bracketsN = "no_brackets";
     3.5  
     3.6  fun no_brackets () =
     3.7 -  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) (! print_mode)
     3.8 -    = SOME no_bracketsN;
     3.9 +  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
    3.10 +    (print_mode_value ()) = SOME no_bracketsN;
    3.11  
    3.12  val type_bracketsN = "type_brackets";
    3.13  val no_type_bracketsN = "no_type_brackets";
    3.14  
    3.15  fun no_type_brackets () =
    3.16 -  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) (! print_mode)
    3.17 -    <> SOME type_bracketsN;
    3.18 +  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
    3.19 +    (print_mode_value ()) <> SOME type_bracketsN;
    3.20  
    3.21  
    3.22  (* parse ast translations *)