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;
Thu, 22 Dec 2022 15:23:26 +0100 wenzelm proper migrate_name between different kinds of Resources, notably for Windows;
Wed, 21 Dec 2022 15:34:33 +0100 wenzelm actually build document;
Wed, 21 Dec 2022 14:00:00 +0100 wenzelm tuned comments;
Tue, 20 Dec 2022 16:34:13 +0100 wenzelm clarified state document nodes for Theories_Status / Document_Dockable;
less more (0) -10 -7 tip