Wed, 29 Jan 2025 20:17:21 +0100 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;
wenzelm [Wed, 29 Jan 2025 20:17:21 +0100] rev 82015
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;
Wed, 29 Jan 2025 14:43:14 +0100 more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');
wenzelm [Wed, 29 Jan 2025 14:43:14 +0100] rev 82014
more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');
Wed, 29 Jan 2025 11:53:49 +0100 more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);
wenzelm [Wed, 29 Jan 2025 11:53:49 +0100] rev 82013
more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 tip