src/Pure/PIDE/markup_tree.scala
Wed, 18 Aug 2010 23:44:50 +0200 wenzelm more efficient Markup_Tree, based on branches sorted by quasi-order;
less more (0) tip