src/Pure/General/pretty.scala
2022-09-08 wenzelm support Pretty.unformatted, similar to ML version;
2022-08-22 wenzelm tuned signature;
2022-04-01 wenzelm clarified formatting, for the sake of scala3;
2021-03-04 wenzelm tuned --- fewer warnings;
2020-04-22 wenzelm tuned signature -- avoid warnings;
2020-03-27 wenzelm misc tuning based on hints by IntelliJ IDEA;
2019-03-05 wenzelm tuned;
2018-03-17 wenzelm clarified signature;
2018-01-30 wenzelm clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
2017-03-06 wenzelm tuned;
2016-04-02 wenzelm proper type;
2016-04-01 wenzelm more robust pretty printing: permissive treatment of bad values;
2015-12-21 wenzelm clarified length of block with pre-existant forced breaks;
2015-12-20 wenzelm unused;
2015-12-20 wenzelm tuned;
2015-12-19 wenzelm more explicit Pretty.Tree, like in ML;
2015-12-19 wenzelm tuned;
2015-12-19 wenzelm tuned signature;
2015-12-19 wenzelm support for blocks with consistent breaks;
2015-12-17 wenzelm support pretty break indent, like underlying ML systems;
2014-02-18 wenzelm tuned signature;
2013-04-04 wenzelm tuned imports;
2013-03-28 wenzelm ghost bullet via markup, which is painted as bar under text (normally space);
2013-03-28 wenzelm 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 maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
2013-03-28 wenzelm tuned;
2013-03-25 wenzelm tuned signature;
2013-03-23 wenzelm allow fractional pretty margin -- avoid premature rounding;
2013-03-23 wenzelm 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);
2013-03-21 wenzelm proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
2013-03-21 wenzelm eliminated char_width_int to avoid unclear rounding;
2013-01-12 wenzelm more uniform Pretty.char_width;
2012-11-25 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-12 wenzelm further refinement of jEdit line range, avoiding lack of final \n;
2012-10-11 wenzelm 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 turn constraints into Isabelle_Markup.typing, depending on show_markup options;
2012-09-28 wenzelm tuned;
2012-09-28 wenzelm support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-20 wenzelm tuned rendering;
2012-09-20 wenzelm tuned signature;
2012-09-18 wenzelm some actual rich text markup via XML.content_markup;
2012-09-18 wenzelm some support for inital command markup;
2012-08-29 wenzelm clarified separated_chunks vs. space_explode;
2012-08-07 wenzelm tuned signature -- make Pretty less dependent on Symbol;
2011-11-28 wenzelm separate module for concrete Isabelle markup;
2011-10-22 wenzelm more private stuff;
2011-07-09 wenzelm tuned signature;
2010-08-25 wenzelm Pretty: tuned markup objects;
2010-08-22 wenzelm tuned signatures;
2010-08-14 wenzelm more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
2010-08-07 wenzelm simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
2010-06-13 wenzelm Pretty.string_of (in Scala): actually observe margin/metric;
2010-05-12 wenzelm clarified Pretty.font_metrics;
2010-05-12 wenzelm tuned;
2010-05-11 wenzelm more precise pretty printing based on actual font metrics;
2010-05-09 wenzelm static Symbol.spaces;
2010-05-08 wenzelm unified/simplified Pretty.margin_default;
2010-05-07 wenzelm unformatted output;
2010-05-07 wenzelm Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
2010-05-06 wenzelm replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
less more (0) -60 tip