src/Pure/PIDE/text.scala
Thu, 26 Aug 2010 11:29:43 +0200 wenzelm tuned signature;
Tue, 24 Aug 2010 23:49:07 +0200 wenzelm Text.Range.is_singleton;
Sun, 22 Aug 2010 19:33:01 +0200 wenzelm misc tuning and simplification;
Sun, 22 Aug 2010 18:46:16 +0200 wenzelm renamed Markup_Tree.Node to Text.Info;
Fri, 20 Aug 2010 22:32:15 +0200 wenzelm added Text.Range.- convenience;
Fri, 20 Aug 2010 12:12:28 +0200 wenzelm alternative constructor for Range singularities;
Fri, 20 Aug 2010 11:00:15 +0200 wenzelm further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
Thu, 19 Aug 2010 22:52:00 +0200 wenzelm parameterized type Markup_Tree.Node;
Thu, 19 Aug 2010 22:26:15 +0200 wenzelm added toString methods;
Thu, 19 Aug 2010 22:04:20 +0200 wenzelm misc tuning and simplification;
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