Tue, 31 Jan 2023 14:59:19 +0100 | wenzelm | defer build until document nodes are ready; | file | diff | annotate |
Tue, 31 Jan 2023 12:27:00 +0100 | wenzelm | clarified Document_Editor.Session: more explicit types, more robust operations; | file | diff | annotate |
Mon, 16 Jan 2023 20:08:15 +0100 | wenzelm | more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup; | file | diff | annotate |