| Wed, 17 Aug 2011 16:01:27 +0200 |
wenzelm |
some convenience actions/shortcuts for control symbols;
|
file |
diff |
annotate
|
| Thu, 07 Jul 2011 13:48:30 +0200 |
wenzelm |
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 23:18:14 +0200 |
wenzelm |
simplified Symbol.iterator: produce strings, which are mostly preallocated;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 22:11:32 +0200 |
wenzelm |
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 18:15:36 +0200 |
wenzelm |
type classes: entity markup instead of old-style token markup;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2011 20:38:03 +0200 |
wenzelm |
clarified decoded control symbols;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2011 14:12:49 +0200 |
wenzelm |
more uniform treatment of recode_set/recode_map;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2011 13:29:44 +0200 |
wenzelm |
tuned iteration over short symbols;
|
file |
diff |
annotate
|
| Sun, 19 Jun 2011 15:31:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 19 Jun 2011 15:22:58 +0200 |
wenzelm |
discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);
|
file |
diff |
annotate
|
| Sun, 19 Jun 2011 14:11:06 +0200 |
wenzelm |
some unicode chars for special control symbols;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 13:52:24 +0200 |
wenzelm |
tuned signatures;
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 16:24:22 +0200 |
wenzelm |
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
|
file |
diff |
annotate
|
| Sat, 07 Aug 2010 22:43:57 +0200 |
wenzelm |
simplified some Markup;
|
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, 30 May 2010 23:40:24 +0200 |
wenzelm |
added HTML.encode (in Scala), similar to HTML.output in ML;
|
file |
diff |
annotate
|
| Tue, 30 Mar 2010 00:47:52 +0200 |
wenzelm |
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 22:55:57 +0200 |
wenzelm |
replaced some deprecated methods;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 22:43:56 +0200 |
wenzelm |
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
|
file |
diff |
annotate
|
| Sat, 19 Dec 2009 16:51:32 +0100 |
wenzelm |
refined some Symbol operations/signatures;
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 13:43:51 +0100 |
wenzelm |
sealed XML.Tree;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 00:02:54 +0100 |
wenzelm |
avoid lazy val with side-effects -- spurious null pointers!?
|
file |
diff |
annotate
|
| Sun, 06 Dec 2009 23:25:27 +0100 |
wenzelm |
proper markup text for loc;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2009 23:08:43 +0100 |
wenzelm |
basic treatment of special control symbols;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2009 22:23:31 +0100 |
wenzelm |
more robust treatment of line breaks -- Java "split" has off semantics;
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 22:51:59 +0100 |
wenzelm |
Basic HTML output.
|
file |
diff |
annotate
|