src/Pure/PIDE/markup.scala
Sun, 23 Feb 2014 14:39:51 +0100 wenzelm clarified completion names;
less more (0) -30 -10 -1 tip