1.1 --- a/src/Pure/General/pretty.ML	Wed Jul 06 20:14:13 2011 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Wed Jul 06 20:46:06 2011 +0200
     1.3 @@ -75,12 +75,13 @@
     1.4  
     1.5  local
     1.6    val default = {indent = default_indent};
     1.7 -  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
     1.8 +  val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
     1.9  in
    1.10 -  fun add_mode name indent = CRITICAL (fn () =>
    1.11 -    Unsynchronized.change modes (Symtab.update_new (name, {indent = indent})));
    1.12 +  fun add_mode name indent =
    1.13 +    Synchronized.change modes (Symtab.update_new (name, {indent = indent}));
    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 mode_indent x y = #indent (get_mode ()) x y;