src/Pure/PIDE/text.scala
Sun, 15 Aug 2010 21:42:13 +0200 wenzelm moved Text_Edit to Text.Edit;
less more (0) tip