src/Pure/General/pretty.ML
2015-12-17 wenzelm 2015-12-17 support pretty break indent, like underlying ML systems;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-05 wenzelm 2014-03-05 unused;
2014-02-26 wenzelm 2014-02-26 tuned signature;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-07-17 wenzelm 2013-07-17 tuned signature;
2013-03-28 wenzelm 2013-03-28 basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
2013-03-25 wenzelm 2013-03-25 clarified text_fold vs. fbrk;
2013-03-23 wenzelm 2013-03-23 tuned;
2012-12-15 wenzelm 2012-12-15 explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-22 wenzelm 2012-11-22 some support for breakable text and paragraphs; tuned Symbol.scanner, which operates on symbols, not characters;
2012-09-29 wenzelm 2012-09-29 treat wrapped markup elements as raw markup delimiters;
2012-09-25 wenzelm 2012-09-25 ML support for generic graph display, with browser and graphview backends (via print modes); reverse graph layout (again), according to the graph orientation provided by ML; simplified scala types -- eliminated unused type parameters; more explicit Model.Info, Model.Graph; renamed isabelle.graphview.Graphview_Frame to isabelle.graphview.Frame in accordance to file name; removed obsolete Graph_XML and Tooltips; tuned graphview command line; more generous JVM resources via GRAPHVIEW_JAVA_OPTIONS;
2012-09-24 wenzelm 2012-09-24 more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;
2012-08-07 wenzelm 2012-08-07 tuned signature -- make Pretty less dependent on Symbol;
2012-03-13 wenzelm 2012-03-13 allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-07-06 wenzelm 2011-07-06 prefer Synchronized.var;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-07 wenzelm 2011-04-07 clarified Pretty.mark; added Pretty.mark_str, Pretty.marks_str convenience;
2010-10-25 wenzelm 2010-10-25 explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-08-18 wenzelm 2010-08-18 uniform Markup.empty/Markup.Empty in ML and Scala;
2010-06-24 wenzelm 2010-06-24 treat Pretty.T as strictly abstract type;
2010-05-30 wenzelm 2010-05-30 simplified command/keyword markup;
2010-05-08 wenzelm 2010-05-08 tuned;
2010-05-08 wenzelm 2010-05-08 discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
2010-05-08 wenzelm 2010-05-08 unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
2010-05-07 wenzelm 2010-05-07 tuned;
2010-05-06 wenzelm 2010-05-06 uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
2010-05-06 wenzelm 2010-05-06 replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
2010-05-06 wenzelm 2010-05-06 basic formatting of pretty trees; line-up ML vs. Scala sources;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
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)