src/Pure/PIDE/xml.scala
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;
less more (0) -3 tip