Tue, 31 Jan 2023 16:13:27 +0100 | wenzelm | more accurate Word.capitalize: do not touch name; | changeset | files |
Tue, 31 Jan 2023 14:59:19 +0100 | wenzelm | defer build until document nodes are ready; | changeset | files |
Tue, 31 Jan 2023 14:37:40 +0100 | wenzelm | clarified signature: prefer semantic status; | changeset | files |
Tue, 31 Jan 2023 14:32:07 +0100 | wenzelm | removed obsolete parameter (see 7c23db6b857b); | changeset | files |
Tue, 31 Jan 2023 12:27:00 +0100 | wenzelm | clarified Document_Editor.Session: more explicit types, more robust operations; | changeset | files |
Mon, 30 Jan 2023 16:26:10 +0100 | wenzelm | more operations; | changeset | files |
Mon, 30 Jan 2023 16:20:17 +0100 | wenzelm | clarified operation (without change of signature!); | changeset | files |
Tue, 31 Jan 2023 19:07:24 +0100 | nipkow | pointless | changeset | files |