src/Pure/General/pretty.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-03-23 wenzelm 2009-03-23 Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode; to_ML/from_ML: proper handling of markup;
2009-03-21 wenzelm 2009-03-21 simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML; removed obsolete pprint;
2009-03-21 wenzelm 2009-03-21 added position; added to_ML, from_ML (approximation);
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-06-25 wenzelm 2008-06-25 pprint: back to proper output of markup, with workaround for Poly/ML crash;
2008-06-24 wenzelm 2008-06-24 back to 1.36 (Poly/ML crash!?);
2008-06-24 wenzelm 2008-06-24 pprint: proper output of markup (important for token translation);
2008-04-17 wenzelm 2008-04-17 removed obsolete raw_str; added mark;
2007-09-17 wenzelm 2007-09-17 avoid direct access to print_mode;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections (for multithreading);
2007-07-11 wenzelm 2007-07-11 Buffer.markup;
2007-07-10 wenzelm 2007-07-10 moved print_mode setup for markup to markup.ML;
2007-07-09 wenzelm 2007-07-09 type output = string indicates raw system output;
2007-07-08 wenzelm 2007-07-08 symbolic output: avoid empty blocks, 1 space for fbreak;
2007-07-08 wenzelm 2007-07-08 export mode_markup; added symbolic output (via print_mode); misc cleanup;
2007-07-07 wenzelm 2007-07-07 added markup_chunks;
2007-07-07 wenzelm 2007-07-07 markup: emit as control information -- no indent text;
2007-07-07 wenzelm 2007-07-07 added print_mode setup: indent and markup; simplified pretty token metric: type int; added general markup for blocks; removed unused writelns;
2007-01-05 haftmann 2007-01-05 added block_enclose
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-14 wenzelm 2006-03-14 added command, keyword; added chunks2;
2006-01-27 wenzelm 2006-01-27 renamed gen_list to enum; added separate; tuned;
2006-01-07 wenzelm 2006-01-07 added backquote;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-21 haftmann 2005-09-21 (name mess cleanup)
2005-09-20 paulson 2005-09-20 fixed recursive-looking declaration
2005-09-15 haftmann 2005-09-15 added gen_list to Pretty module
2005-07-06 wenzelm 2005-07-06 added output_buffer;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2004-06-22 wenzelm 2004-06-22 added output, removed pp_undef;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-20 wenzelm 2004-06-20 tuned;
2004-05-29 wenzelm 2004-05-29 pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
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;