src/Pure/PIDE/document_editor.scala
Tue, 31 Jan 2023 14:59:19 +0100 wenzelm defer build until document nodes are ready;
Tue, 31 Jan 2023 12:27:00 +0100 wenzelm clarified Document_Editor.Session: more explicit types, more robust operations;
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;
less more (0) -10 -3 tip