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