src/Pure/General/print_mode.ML
changeset 32738 15bb09ca0378
parent 29606 fedb8be05f24
child 33223 d27956b4d3b4
     1.1 --- a/src/Pure/General/print_mode.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/General/print_mode.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -7,9 +7,9 @@
     1.4  
     1.5  signature BASIC_PRINT_MODE =
     1.6  sig
     1.7 -  val print_mode: string list ref            (*global template*)
     1.8 -  val print_mode_value: unit -> string list  (*thread-local value*)
     1.9 -  val print_mode_active: string -> bool      (*thread-local value*)
    1.10 +  val print_mode: string list Unsynchronized.ref  (*global template*)
    1.11 +  val print_mode_value: unit -> string list       (*thread-local value*)
    1.12 +  val print_mode_active: string -> bool           (*thread-local value*)
    1.13  end;
    1.14  
    1.15  signature PRINT_MODE =
    1.16 @@ -28,7 +28,7 @@
    1.17  val input = "input";
    1.18  val internal = "internal";
    1.19  
    1.20 -val print_mode = ref ([]: string list);
    1.21 +val print_mode = Unsynchronized.ref ([]: string list);
    1.22  val tag = Universal.tag () : string list option Universal.tag;
    1.23  
    1.24  fun print_mode_value () =