1.1 --- a/src/Pure/General/markup.ML	Wed Jul 06 20:14:13 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Wed Jul 06 20:46:06 2011 +0200
     1.3 @@ -378,12 +378,13 @@
     1.4  
     1.5  local
     1.6    val default = {output = default_output};
     1.7 -  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
     1.8 +  val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
     1.9  in
    1.10 -  fun add_mode name output = CRITICAL (fn () =>
    1.11 -    Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
    1.12 +  fun add_mode name output =
    1.13 +    Synchronized.change modes (Symtab.update_new (name, {output = output}));
    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 m = if is_empty m then no_output else #output (get_mode ()) m;