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);

clarifed terminology

extracted the ^^ subtheory for modularity reasons

tuned

merged

tuned;