src/Pure/PIDE/markup_tree.scala
Mon, 23 Aug 2010 20:50:00 +0200 wenzelm misc tuning of important special cases;
less more (0) -10 -1 tip