src/Pure/ML/ml_print_depth.ML
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-04-14 wenzelm 2016-04-14 tuned headers;
2016-04-07 wenzelm 2016-04-07 simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;