| Wed, 29 Jan 2025 20:52:27 +0100 | wenzelm | rebuild jedit component; | changeset | files |
| Wed, 29 Jan 2025 20:17:21 +0100 | wenzelm | 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; | changeset | files |
| Wed, 29 Jan 2025 14:43:14 +0100 | wenzelm | more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts'); | changeset | files |
| Wed, 29 Jan 2025 11:53:49 +0100 | wenzelm | more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25); | changeset | files |
| Tue, 28 Jan 2025 21:42:51 +0100 | haftmann | clarifed terminology | changeset | files |
| Tue, 28 Jan 2025 21:42:04 +0100 | nipkow | extracted the ^^ subtheory for modularity reasons | changeset | files |