1.1 --- a/src/Pure/General/pretty.ML	Mon Mar 12 23:33:50 2012 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Tue Mar 13 11:21:26 2012 +0100
     1.3 @@ -78,7 +78,10 @@
     1.4    val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
     1.5  in
     1.6    fun add_mode name indent =
     1.7 -    Synchronized.change modes (Symtab.update_new (name, {indent = indent}));
     1.8 +    Synchronized.change modes (fn tab =>
     1.9 +      (if not (Symtab.defined tab name) then ()
    1.10 +       else warning ("Redefining pretty mode " ^ quote name);
    1.11 +       Symtab.update (name, {indent = indent}) tab));
    1.12    fun get_mode () =
    1.13      the_default default
    1.14        (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));

     2.1 --- a/src/Pure/PIDE/markup.ML	Mon Mar 12 23:33:50 2012 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Tue Mar 13 11:21:26 2012 +0100
     2.3 @@ -74,7 +74,10 @@
     2.4    val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
     2.5  in
     2.6    fun add_mode name output =
     2.7 -    Synchronized.change modes (Symtab.update_new (name, {output = output}));
     2.8 +    Synchronized.change modes (fn tab =>
     2.9 +      (if not (Symtab.defined tab name) then ()
    2.10 +       else warning ("Redefining markup mode " ^ quote name);
    2.11 +       Symtab.update (name, {output = output}) tab));
    2.12    fun get_mode () =
    2.13      the_default default
    2.14        (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));