| 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 |