src/Pure/PIDE/resources.scala
Sat, 29 Mar 2014 10:49:32 +0100 wenzelm propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
Sat, 29 Mar 2014 10:17:09 +0100 wenzelm tuned signature;
Sat, 29 Mar 2014 09:34:51 +0100 wenzelm tuned signature;
Tue, 18 Mar 2014 17:53:40 +0100 wenzelm simplified (despite 70898d016538);
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
less more (0) tip