Wed, 29 Aug 2012 12:55:41 +0200 |
wenzelm |
clarified separated_chunks vs. space_explode;
|
file |
diff |
annotate
|
Tue, 07 Aug 2012 12:10:26 +0200 |
wenzelm |
tuned signature -- make Pretty less dependent on Symbol;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
Sat, 22 Oct 2011 23:30:02 +0200 |
wenzelm |
more private stuff;
|
file |
diff |
annotate
|
Sat, 09 Jul 2011 12:56:51 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 22:57:40 +0200 |
wenzelm |
Pretty: tuned markup objects;
|
file |
diff |
annotate
|
Sun, 22 Aug 2010 13:52:24 +0200 |
wenzelm |
tuned signatures;
|
file |
diff |
annotate
|
Sat, 14 Aug 2010 22:45:23 +0200 |
wenzelm |
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
|
file |
diff |
annotate
|
Sat, 07 Aug 2010 22:09:52 +0200 |
wenzelm |
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
|
file |
diff |
annotate
|
Sun, 13 Jun 2010 23:04:09 +0200 |
wenzelm |
Pretty.string_of (in Scala): actually observe margin/metric;
|
file |
diff |
annotate
|
Wed, 12 May 2010 12:50:00 +0200 |
wenzelm |
clarified Pretty.font_metrics;
|
file |
diff |
annotate
|
Wed, 12 May 2010 11:28:52 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 11 May 2010 23:36:06 +0200 |
wenzelm |
more precise pretty printing based on actual font metrics;
|
file |
diff |
annotate
|
Sun, 09 May 2010 13:12:22 +0200 |
wenzelm |
static Symbol.spaces;
|
file |
diff |
annotate
|
Sat, 08 May 2010 19:14:13 +0200 |
wenzelm |
unified/simplified Pretty.margin_default;
|
file |
diff |
annotate
|
Fri, 07 May 2010 22:27:28 +0200 |
wenzelm |
unformatted output;
|
file |
diff |
annotate
|
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;
|
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
|
Thu, 06 May 2010 16:27:47 +0200 |
wenzelm |
basic support for symbolic pretty printing;
|
file |
diff |
annotate
|