tuned output;

suppress MacOS.jar from jEdit 5.7.0, following 65fd0f032a75;

tuned GUI: attempt to improve divider mobility;

rebuild jedit component;

make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;

more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');

more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);