src/Pure/General/pretty.scala
2015-12-17 wenzelm 2015-12-17 support pretty break indent, like underlying ML systems;
2014-02-18 wenzelm 2014-02-18 tuned signature;
2013-04-04 wenzelm 2013-04-04 tuned imports;
2013-03-28 wenzelm 2013-03-28 ghost bullet via markup, which is painted as bar under text (normally space);
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-28 wenzelm 2013-03-28 maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually; always round block indentation upwards, to ensure that text moves visually to the right of the "hanging" part;
2013-03-28 wenzelm 2013-03-28 tuned;
2013-03-25 wenzelm 2013-03-25 tuned signature;
2013-03-23 wenzelm 2013-03-23 allow fractional pretty margin -- avoid premature rounding;
2013-03-23 wenzelm 2013-03-23 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb); separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;
2013-03-21 wenzelm 2013-03-21 proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
2013-03-21 wenzelm 2013-03-21 eliminated char_width_int to avoid unclear rounding; clarified integer conversion for margin;
2013-01-12 wenzelm 2013-01-12 more uniform Pretty.char_width;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-12 wenzelm 2012-10-12 further refinement of jEdit line range, avoiding lack of final \n;
2012-10-11 wenzelm 2012-10-11 refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
2012-09-29 wenzelm 2012-09-29 turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format;
2012-09-28 wenzelm 2012-09-28 tuned;
2012-09-28 wenzelm 2012-09-28 support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-20 wenzelm 2012-09-20 tuned rendering;
2012-09-20 wenzelm 2012-09-20 tuned signature;
2012-09-18 wenzelm 2012-09-18 some actual rich text markup via XML.content_markup; tuned signature;
2012-09-18 wenzelm 2012-09-18 some support for inital command markup; tuned signature;
2012-08-29 wenzelm 2012-08-29 clarified separated_chunks vs. space_explode;
2012-08-07 wenzelm 2012-08-07 tuned signature -- make Pretty less dependent on Symbol;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-10-22 wenzelm 2011-10-22 more private stuff;
2011-07-09 wenzelm 2011-07-09 tuned signature;
2010-08-25 wenzelm 2010-08-25 Pretty: tuned markup objects;
2010-08-22 wenzelm 2010-08-22 tuned signatures;
2010-08-14 wenzelm 2010-08-14 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;
2010-08-07 wenzelm 2010-08-07 simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; XML.cache_tree: actually store XML.Text as well; added Isabelle_Process.Result.properties;
2010-06-13 wenzelm 2010-06-13 Pretty.string_of (in Scala): actually observe margin/metric;
2010-05-12 wenzelm 2010-05-12 clarified Pretty.font_metrics;
2010-05-12 wenzelm 2010-05-12 tuned;
2010-05-11 wenzelm 2010-05-11 more precise pretty printing based on actual font metrics; removed obsolete relative margin;
2010-05-09 wenzelm 2010-05-09 static Symbol.spaces;
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 unformatted output;
2010-05-07 wenzelm 2010-05-07 Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version; tuned;
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;
2010-05-06 wenzelm 2010-05-06 basic support for symbolic pretty printing; tuned;