1.1 --- a/src/Pure/General/output.ML	Wed Jul 06 20:14:13 2011 +0200
     1.2 +++ b/src/Pure/General/output.ML	Wed Jul 06 20:46:06 2011 +0200
     1.3 @@ -55,12 +55,13 @@
     1.4  
     1.5  local
     1.6    val default = {output = default_output, escape = default_escape};
     1.7 -  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
     1.8 +  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
     1.9  in
    1.10 -  fun add_mode name output escape = CRITICAL (fn () =>
    1.11 -    Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
    1.12 +  fun add_mode name output escape =
    1.13 +    Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
    1.14    fun get_mode () =
    1.15 -    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    1.16 +    the_default default
    1.17 +      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
    1.18  end;
    1.19  
    1.20  fun output_width x = #output (get_mode ()) x;