jEdit 5.2pre1 / Highlight 1.9.12 doesn’t load anymore:
This looks like somebody had a bright idea and removed some API that has become part of the Java platform without checking for any uses of that API. Now would that somebody care to fix the Highlight plugin, please? Or at least explain how to replace that API? Thanks a lot!