src/Pure/General/print_mode.ML
changeset 62889 99c7f31615c2
parent 62542 b27b7c2200b9
     1.1 --- a/src/Pure/General/print_mode.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Pure/General/print_mode.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -34,20 +34,18 @@
     1.4  val internal = "internal";
     1.5  
     1.6  val print_mode = Unsynchronized.ref ([]: string list);
     1.7 -val tag = Universal.tag () : string list option Universal.tag;
     1.8 +val print_mode_var = Thread_Data.var () : string list Thread_Data.var;
     1.9  
    1.10  fun print_mode_value () =
    1.11    let val modes =
    1.12 -    (case Thread.getLocal tag of
    1.13 -      SOME (SOME modes) => modes
    1.14 -    | _ => ! print_mode)
    1.15 +    (case Thread_Data.get print_mode_var of
    1.16 +      SOME modes => modes
    1.17 +    | NONE => ! print_mode)
    1.18    in subtract (op =) [input, internal] modes end;
    1.19  
    1.20  fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
    1.21  
    1.22 -fun setmp modes f x =
    1.23 -  let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE)
    1.24 -  in setmp_thread_data tag orig_modes (SOME modes) f x end;
    1.25 +fun setmp modes f x = Thread_Data.setmp print_mode_var (SOME modes) f x;
    1.26  
    1.27  fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
    1.28  fun closure f = with_modes [] f;