src/Tools/jEdit/src/jedit_resources.scala
2014-04-09 wenzelm 2014-04-09 improved support for external URLs, based on standard Java network operations;
2014-04-08 wenzelm 2014-04-08 ignore deps_changed (again) -- avoid proactive load attempts of unfinished header specification while the user is typing;
2014-04-07 wenzelm 2014-04-07 tuned signature -- prefer static type Document.Node.Name;
2014-03-29 wenzelm 2014-03-29 propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save); tuned signature;
2014-03-18 wenzelm 2014-03-18 clarifed module name;