src/Pure/PIDE/markup_node.scala
Wed, 05 May 2010 23:55:29 +0200 wenzelm eliminated deprecated "--" method;
Wed, 05 May 2010 22:23:45 +0200 wenzelm some rearrangement of Scala sources;
less more (0) tip