| 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
|
| 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:40:44 +0200 |
wenzelm |
Markup_Tree.select: crude version of stream-based filtering;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 12:41:40 +0200 |
wenzelm |
tuned Markup_Tree, using SortedMap more carefully;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 23:44:50 +0200 |
wenzelm |
more efficient Markup_Tree, based on branches sorted by quasi-order;
|
file |
diff |
annotate
| base
|