src/Pure/PIDE/text_edit.scala
Thu, 05 Aug 2010 18:17:59 +0200 wenzelm Text_Edit.convert/revert;
Wed, 05 May 2010 22:23:45 +0200 wenzelm some rearrangement of Scala sources;
less more (0) tip