src/Pure/PIDE/xml.scala
Tue, 18 Sep 2012 15:55:29 +0200 wenzelm recover order of stacked markup;
Tue, 18 Sep 2012 14:51:12 +0200 wenzelm some actual rich text markup via XML.content_markup;
Thu, 08 Mar 2012 21:36:36 +0100 wenzelm simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
Tue, 29 Nov 2011 21:29:53 +0100 wenzelm separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
Mon, 28 Nov 2011 22:18:19 +0100 wenzelm explicit indication of modules for independent Scala library;
Wed, 07 Sep 2011 23:08:04 +0200 wenzelm XML.cache for partial sharing (strings only);
Mon, 05 Sep 2011 20:30:37 +0200 wenzelm tuned imports;
less more (0) -7 tip