src/Pure/General/print_mode.ML
Mon, 17 Sep 2007 16:36:43 +0200 wenzelm added print_mode_value (CRITICAL);
Sun, 16 Sep 2007 15:27:26 +0200 wenzelm with_modes: always CRITICAL;
Mon, 20 Aug 2007 20:44:02 +0200 wenzelm with_modes []: non-critical;
Sun, 29 Jul 2007 17:28:55 +0200 wenzelm NAMED_CRITICAL;
Mon, 23 Jul 2007 16:45:02 +0200 wenzelm added with_modes, with_default;
Tue, 17 Jul 2007 13:19:39 +0200 wenzelm Generic print mode.
less more (0) tip