src/Pure/General/print_mode.ML
2007-12-20 wenzelm 2007-12-20 separated into global template vs. thread-local value; made setmp thread-local (non-critical); added closure;
2007-10-20 wenzelm 2007-10-20 added input/internal, which are never active in print_mode_value;
2007-09-18 wenzelm 2007-09-18 simplified PrintMode interfaces;
2007-09-17 wenzelm 2007-09-17 added print_mode_value (CRITICAL);
2007-09-16 wenzelm 2007-09-16 with_modes: always CRITICAL;
2007-08-20 wenzelm 2007-08-20 with_modes []: non-critical;
2007-07-29 wenzelm 2007-07-29 NAMED_CRITICAL;
2007-07-23 wenzelm 2007-07-23 added with_modes, with_default;
2007-07-17 wenzelm 2007-07-17 Generic print mode.