changeset 24612 | d1b315bdb8d7 |
parent 24555 | ea220faa69e7 |
child 24777 | c1250851d701 |
--- a/src/Pure/General/markup.ML Mon Sep 17 16:06:35 2007 +0200 +++ b/src/Pure/General/markup.ML Mon Sep 17 16:36:41 2007 +0200 @@ -170,7 +170,7 @@ fun add_mode name output = CRITICAL (fn () => change modes (Symtab.update_new (name, {output = output}))); fun get_mode () = - the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode)); + the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ())); end; fun output ("", _) = ("", "")