src/Pure/General/print_mode.ML
2007-07-17 wenzelm 2007-07-17 Generic print mode.