src/Pure/General/pretty.ML
Thu, 07 Apr 2016 13:35:08 +0200 wenzelm clarified bootstrap of @{make_string} -- avoid query on ML environment;
Sat, 02 Apr 2016 22:38:26 +0200 wenzelm tuned signature;
Sat, 02 Apr 2016 21:54:51 +0200 wenzelm proper type;
Sat, 02 Apr 2016 21:10:07 +0200 wenzelm careful export of type-dependent functions, without losing their special status;
Fri, 01 Apr 2016 14:38:54 +0200 wenzelm more robust pretty printing: permissive treatment of bad values;
Fri, 01 Apr 2016 11:45:04 +0200 wenzelm adapted to Poly/ML repository version 2e40cadc975a;
Thu, 31 Mar 2016 23:36:33 +0200 wenzelm explicit mixfix block properties;
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;
less more (0) -50 -30 tip