# HG changeset patch
# User wenzelm
# Date 1331634086 -3600
# Node ID e2ad717ec889d98a33d9a8e0bda7ee31e27b3dcd
# Parent  d5bb4c212df16c6065c8095787d6fc1010bc0e5f
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;

diff -r d5bb4c212df1 -r e2ad717ec889 src/Pure/General/pretty.ML
--- 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 ()));
diff -r d5bb4c212df1 -r e2ad717ec889 src/Pure/PIDE/markup.ML
--- 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 ()));