allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;

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

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