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