src/Pure/PIDE/markup_tree.scala
Sat, 13 Jul 2013 12:39:45 +0200 wenzelm full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
less more (0) -30 -10 -1 tip