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);