src/Pure/PIDE/text.scala
Thu, 19 Aug 2010 17:37:13 +0200 wenzelm Text.Range: improved handling of singularities;
Wed, 18 Aug 2010 14:02:32 +0200 wenzelm refined notion of Text.Range;
Sun, 15 Aug 2010 23:07:22 +0200 wenzelm some derived operations on Text.Range;
Sun, 15 Aug 2010 22:48:56 +0200 wenzelm specific types Text.Offset and Text.Range;
Sun, 15 Aug 2010 21:42:13 +0200 wenzelm moved Text_Edit to Text.Edit;
less more (0) tip