src/Pure/PIDE/resources.scala
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
less more (0) tip