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; | file | diff | annotate |
Thu, 19 Aug 2010 22:52:00 +0200 | wenzelm | parameterized type Markup_Tree.Node; | file | diff | annotate |
Thu, 19 Aug 2010 22:26:15 +0200 | wenzelm | added toString methods; | file | diff | annotate |
Thu, 19 Aug 2010 22:04:20 +0200 | wenzelm | misc tuning and simplification; | file | diff | annotate |
Thu, 19 Aug 2010 17:37:13 +0200 | wenzelm | Text.Range: improved handling of singularities; | file | diff | annotate |
Wed, 18 Aug 2010 14:02:32 +0200 | wenzelm | refined notion of Text.Range; | file | diff | annotate |
Sun, 15 Aug 2010 23:07:22 +0200 | wenzelm | some derived operations on Text.Range; | file | diff | annotate |
Sun, 15 Aug 2010 22:48:56 +0200 | wenzelm | specific types Text.Offset and Text.Range; | file | diff | annotate |
Sun, 15 Aug 2010 21:42:13 +0200 | wenzelm | moved Text_Edit to Text.Edit; | file | diff | annotate | base |