src/Pure/General/pretty.ML
Fri, 18 Mar 2016 21:21:09 +0100 wenzelm clarified print depth;
Fri, 18 Mar 2016 17:51:57 +0100 wenzelm clarified Pretty.T toplevel pp;
Fri, 18 Mar 2016 16:26:35 +0100 wenzelm clarified modules;
Tue, 23 Feb 2016 16:20:12 +0100 wenzelm support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
Wed, 20 Jan 2016 14:32:56 +0100 wenzelm tuned signature (according to Scala version);
Thu, 07 Jan 2016 16:10:13 +0100 wenzelm prefer non-ASCII output;
Mon, 21 Dec 2015 13:39:45 +0100 wenzelm clarified length of block with pre-existant forced breaks;
Sun, 20 Dec 2015 13:06:26 +0100 wenzelm renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
Sat, 19 Dec 2015 22:25:01 +0100 wenzelm tuned;
Sat, 19 Dec 2015 19:52:52 +0100 wenzelm clarified underlying datatypes;
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;
Sat, 19 Dec 2015 10:59:14 +0100 wenzelm preserve break indentation;
Thu, 17 Dec 2015 17:32:01 +0100 wenzelm support pretty break indent, like underlying ML systems;
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Wed, 05 Mar 2014 16:06:11 +0100 wenzelm unused;
Wed, 26 Feb 2014 10:53:19 +0100 wenzelm tuned signature;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
Wed, 17 Jul 2013 23:32:28 +0200 wenzelm tuned signature;
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.);
Mon, 25 Mar 2013 14:04:01 +0100 wenzelm clarified text_fold vs. fbrk;
Sat, 23 Mar 2013 13:04:28 +0100 wenzelm tuned;
Sat, 15 Dec 2012 12:55:11 +0100 wenzelm explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Thu, 22 Nov 2012 12:22:03 +0100 wenzelm some support for breakable text and paragraphs;
Sat, 29 Sep 2012 16:15:18 +0200 wenzelm treat wrapped markup elements as raw markup delimiters;
Tue, 25 Sep 2012 20:28:47 +0200 wenzelm ML support for generic graph display, with browser and graphview backends (via print modes);
Mon, 24 Sep 2012 17:28:36 +0200 wenzelm more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;
Tue, 07 Aug 2012 12:10:26 +0200 wenzelm tuned signature -- make Pretty less dependent on Symbol;
Tue, 13 Mar 2012 11:21:26 +0100 wenzelm allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Wed, 06 Jul 2011 20:46:06 +0200 wenzelm prefer Synchronized.var;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Thu, 07 Apr 2011 17:38:17 +0200 wenzelm clarified Pretty.mark;
Mon, 25 Oct 2010 20:24:13 +0200 wenzelm explicitly qualify type Output.output, which is a slightly odd internal feature;
Wed, 18 Aug 2010 11:02:47 +0200 wenzelm uniform Markup.empty/Markup.Empty in ML and Scala;
Thu, 24 Jun 2010 14:31:46 +0200 wenzelm treat Pretty.T as strictly abstract type;
Sun, 30 May 2010 14:21:35 +0200 wenzelm simplified command/keyword markup;
Sat, 08 May 2010 20:12:49 +0200 wenzelm tuned;
Sat, 08 May 2010 19:53:11 +0200 wenzelm discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
Sat, 08 May 2010 19:14:13 +0200 wenzelm unified/simplified Pretty.margin_default;
Fri, 07 May 2010 20:16:46 +0200 wenzelm tuned;
Thu, 06 May 2010 23:57:55 +0200 wenzelm uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
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;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Mon, 23 Mar 2009 15:23:06 +0100 wenzelm Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
Sat, 21 Mar 2009 19:58:45 +0100 wenzelm simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
Sat, 21 Mar 2009 15:08:00 +0100 wenzelm added position;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Wed, 25 Jun 2008 12:15:05 +0200 wenzelm pprint: back to proper output of markup, with workaround for Poly/ML crash;
Tue, 24 Jun 2008 23:38:44 +0200 wenzelm back to 1.36 (Poly/ML crash!?);
Tue, 24 Jun 2008 21:44:52 +0200 wenzelm pprint: proper output of markup (important for token translation);
Thu, 17 Apr 2008 16:30:48 +0200 wenzelm removed obsolete raw_str;
Mon, 17 Sep 2007 16:36:41 +0200 wenzelm avoid direct access to print_mode;
Mon, 23 Jul 2007 14:06:12 +0200 wenzelm marked some CRITICAL sections (for multithreading);
Wed, 11 Jul 2007 17:47:49 +0200 wenzelm Buffer.markup;
Tue, 10 Jul 2007 16:45:00 +0200 wenzelm moved print_mode setup for markup to markup.ML;
less more (0) -60 tip