src/Pure/General/pretty.ML
2001-12-08 wenzelm 2001-12-08 added writelns;
2001-01-21 wenzelm 2001-01-21 support general indentation (e.g. for non-tt latex output); tuned;
2000-08-29 wenzelm 2000-08-29 added indent;
2000-06-25 wenzelm 2000-06-25 fbrk: 2 if not taken;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-03-15 wenzelm 2000-03-15 removed lst, strlen, strlen_real, spc, sym; added chunks, raw_str; pass all strings through Symbol.output (beware: this is done at different times for str and spacing/linebreaks!); speedup formatting (uses Buffer.T); tuned;
1999-03-09 wenzelm 1999-03-09 added strlen_real, setmp_margin;
1999-02-11 wenzelm 1999-02-11 sym: Symbol.output_width;
1999-01-13 wenzelm 1999-01-13 fixed titles;
1999-01-13 wenzelm 1999-01-13 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;