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