src/Pure/PIDE/editor.scala
Mon, 12 Aug 2013 11:39:29 +0200 wenzelm tuned signature -- more abstract PIDE editor operations;
less more (0) tip