src/Pure/General/pretty.scala
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Wed, 22 Apr 2020 17:52:14 +0200 wenzelm tuned signature -- avoid warnings;
Fri, 27 Mar 2020 22:01:27 +0100 wenzelm misc tuning based on hints by IntelliJ IDEA;
Tue, 05 Mar 2019 18:44:02 +0100 wenzelm tuned;
Sat, 17 Mar 2018 20:35:23 +0100 wenzelm clarified signature;
Tue, 30 Jan 2018 23:01:38 +0100 wenzelm clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
Mon, 06 Mar 2017 17:05:57 +0100 wenzelm tuned;
Sat, 02 Apr 2016 21:54:51 +0200 wenzelm proper type;
Fri, 01 Apr 2016 14:38:54 +0200 wenzelm more robust pretty printing: permissive treatment of bad values;
Mon, 21 Dec 2015 13:39:45 +0100 wenzelm clarified length of block with pre-existant forced breaks;
Sun, 20 Dec 2015 12:50:48 +0100 wenzelm unused;
Sun, 20 Dec 2015 12:48:56 +0100 wenzelm tuned;
Sat, 19 Dec 2015 23:16:47 +0100 wenzelm more explicit Pretty.Tree, like in ML;
Sat, 19 Dec 2015 19:07:14 +0100 wenzelm tuned;
Sat, 19 Dec 2015 15:14:59 +0100 wenzelm tuned signature;
Sat, 19 Dec 2015 14:47:52 +0100 wenzelm support for blocks with consistent breaks;
Thu, 17 Dec 2015 17:32:01 +0100 wenzelm support pretty break indent, like underlying ML systems;
Tue, 18 Feb 2014 17:03:12 +0100 wenzelm tuned signature;
Thu, 04 Apr 2013 17:16:51 +0200 wenzelm tuned imports;
Thu, 28 Mar 2013 22:42:18 +0100 wenzelm ghost bullet via markup, which is painted as bar under text (normally space);
Thu, 28 Mar 2013 15:36:45 +0100 wenzelm basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
Thu, 28 Mar 2013 15:00:27 +0100 wenzelm maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
Thu, 28 Mar 2013 14:47:37 +0100 wenzelm tuned;
Mon, 25 Mar 2013 10:37:38 +0100 wenzelm tuned signature;
Sat, 23 Mar 2013 13:57:46 +0100 wenzelm allow fractional pretty margin -- avoid premature rounding;
Sat, 23 Mar 2013 13:12:39 +0100 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);
Thu, 21 Mar 2013 16:58:14 +0100 wenzelm proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
Thu, 21 Mar 2013 16:35:53 +0100 wenzelm eliminated char_width_int to avoid unclear rounding;
Sat, 12 Jan 2013 19:53:24 +0100 wenzelm more uniform Pretty.char_width;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Fri, 12 Oct 2012 23:38:48 +0200 wenzelm further refinement of jEdit line range, avoiding lack of final \n;
Thu, 11 Oct 2012 23:10:49 +0200 wenzelm refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
Sat, 29 Sep 2012 16:17:46 +0200 wenzelm turn constraints into Isabelle_Markup.typing, depending on show_markup options;
Fri, 28 Sep 2012 23:02:39 +0200 wenzelm tuned;
Fri, 28 Sep 2012 22:53:18 +0200 wenzelm support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
Thu, 20 Sep 2012 21:31:56 +0200 wenzelm tuned rendering;
Thu, 20 Sep 2012 15:00:14 +0200 wenzelm tuned signature;
Tue, 18 Sep 2012 14:51:12 +0200 wenzelm some actual rich text markup via XML.content_markup;
Tue, 18 Sep 2012 13:18:45 +0200 wenzelm some support for inital command markup;
Wed, 29 Aug 2012 12:55:41 +0200 wenzelm clarified separated_chunks vs. space_explode;
Tue, 07 Aug 2012 12:10:26 +0200 wenzelm tuned signature -- make Pretty less dependent on Symbol;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Sat, 22 Oct 2011 23:30:02 +0200 wenzelm more private stuff;
Sat, 09 Jul 2011 12:56:51 +0200 wenzelm tuned signature;
Wed, 25 Aug 2010 22:57:40 +0200 wenzelm Pretty: tuned markup objects;
Sun, 22 Aug 2010 13:52:24 +0200 wenzelm tuned signatures;
Sat, 14 Aug 2010 22:45:23 +0200 wenzelm more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
Sat, 07 Aug 2010 22:09:52 +0200 wenzelm simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
Sun, 13 Jun 2010 23:04:09 +0200 wenzelm Pretty.string_of (in Scala): actually observe margin/metric;
Wed, 12 May 2010 12:50:00 +0200 wenzelm clarified Pretty.font_metrics;
Wed, 12 May 2010 11:28:52 +0200 wenzelm tuned;
Tue, 11 May 2010 23:36:06 +0200 wenzelm more precise pretty printing based on actual font metrics;
Sun, 09 May 2010 13:12:22 +0200 wenzelm static Symbol.spaces;
Sat, 08 May 2010 19:14:13 +0200 wenzelm unified/simplified Pretty.margin_default;
Fri, 07 May 2010 22:27:28 +0200 wenzelm unformatted output;
Fri, 07 May 2010 20:57:37 +0200 wenzelm Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
Thu, 06 May 2010 23:52:20 +0200 wenzelm replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
Thu, 06 May 2010 23:07:21 +0200 wenzelm basic formatting of pretty trees;
Thu, 06 May 2010 16:27:47 +0200 wenzelm basic support for symbolic pretty printing;
less more (0) tip