| Wed, 17 Jul 2013 23:32:28 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 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.);
|
file |
diff |
annotate
|
| Mon, 25 Mar 2013 14:04:01 +0100 |
wenzelm |
clarified text_fold vs. fbrk;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 13:04:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 12:55:11 +0100 |
wenzelm |
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 12:22:03 +0100 |
wenzelm |
some support for breakable text and paragraphs;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 16:15:18 +0200 |
wenzelm |
treat wrapped markup elements as raw markup delimiters;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2012 20:28:47 +0200 |
wenzelm |
ML support for generic graph display, with browser and graphview backends (via print modes);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 12:10:26 +0200 |
wenzelm |
tuned signature -- make Pretty less dependent on Symbol;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 20:46:06 +0200 |
wenzelm |
prefer Synchronized.var;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 17:38:17 +0200 |
wenzelm |
clarified Pretty.mark;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 20:24:13 +0200 |
wenzelm |
explicitly qualify type Output.output, which is a slightly odd internal feature;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 11:02:47 +0200 |
wenzelm |
uniform Markup.empty/Markup.Empty in ML and Scala;
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 14:31:46 +0200 |
wenzelm |
treat Pretty.T as strictly abstract type;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 14:21:35 +0200 |
wenzelm |
simplified command/keyword markup;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 20:12:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 19:14:13 +0200 |
wenzelm |
unified/simplified Pretty.margin_default;
|
file |
diff |
annotate
|
| Fri, 07 May 2010 20:16:46 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 06 May 2010 23:07:21 +0200 |
wenzelm |
basic formatting of pretty trees;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 19:58:45 +0100 |
wenzelm |
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 15:08:00 +0100 |
wenzelm |
added position;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 12:15:05 +0200 |
wenzelm |
pprint: back to proper output of markup, with workaround for Poly/ML crash;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 23:38:44 +0200 |
wenzelm |
back to 1.36 (Poly/ML crash!?);
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 21:44:52 +0200 |
wenzelm |
pprint: proper output of markup (important for token translation);
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 16:30:48 +0200 |
wenzelm |
removed obsolete raw_str;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2007 16:36:41 +0200 |
wenzelm |
avoid direct access to print_mode;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 14:06:12 +0200 |
wenzelm |
marked some CRITICAL sections (for multithreading);
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 17:47:49 +0200 |
wenzelm |
Buffer.markup;
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 16:45:00 +0200 |
wenzelm |
moved print_mode setup for markup to markup.ML;
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 11:44:20 +0200 |
wenzelm |
type output = string indicates raw system output;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:52:10 +0200 |
wenzelm |
symbolic output: avoid empty blocks, 1 space for fbreak;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 13:10:54 +0200 |
wenzelm |
export mode_markup;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 18:39:18 +0200 |
wenzelm |
added markup_chunks;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 12:16:16 +0200 |
wenzelm |
markup: emit as control information -- no indent text;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 00:14:58 +0200 |
wenzelm |
added print_mode setup: indent and markup;
|
file |
diff |
annotate
|
| Fri, 05 Jan 2007 14:31:48 +0100 |
haftmann |
added block_enclose
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 22:06:35 +0100 |
wenzelm |
added command, keyword;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:08 +0100 |
wenzelm |
renamed gen_list to enum;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 12:26:27 +0100 |
wenzelm |
added backquote;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 10:39:38 +0200 |
haftmann |
(name mess cleanup)
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 18:47:42 +0200 |
paulson |
fixed recursive-looking declaration
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 07:35:38 +0200 |
haftmann |
added gen_list to Pretty module
|
file |
diff |
annotate
|
| Wed, 06 Jul 2005 10:41:48 +0200 |
wenzelm |
added output_buffer;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Tue, 22 Jun 2004 09:51:59 +0200 |
wenzelm |
added output, removed pp_undef;
|
file |
diff |
annotate
|