| Sun, 22 Aug 2010 18:46:16 +0200 | wenzelm | renamed Markup_Tree.Node to Text.Info; | file | diff | annotate |
| Sun, 22 Aug 2010 16:43:20 +0200 | wenzelm | removed obsolete Markup_Tree.flatten/filter; | file | diff | annotate |
| Fri, 20 Aug 2010 22:35:01 +0200 | wenzelm | Markup_Tree.select: misc simplification, proper restriction of parent in subtree; | file | diff | annotate |
| Fri, 20 Aug 2010 12:12:28 +0200 | wenzelm | alternative constructor for Range singularities; | file | diff | annotate |
| Fri, 20 Aug 2010 11:47:33 +0200 | wenzelm | Branches.overlapping: proper treatment of stop_range that overlaps with end; | file | diff | annotate |
| Thu, 19 Aug 2010 22:52:00 +0200 | wenzelm | parameterized type Markup_Tree.Node; | file | diff | annotate |