src/Pure/PIDE/document_editor.scala
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;
Tue, 20 Dec 2022 13:59:07 +0100 wenzelm clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
Sun, 18 Dec 2022 15:49:37 +0100 wenzelm clarified signature;
Thu, 08 Dec 2022 22:38:03 +0100 wenzelm clarified signature: proper scopes and types;
Thu, 08 Dec 2022 22:11:36 +0100 wenzelm maintain global state of document editor views, notably for is_active operation;
Thu, 08 Dec 2022 17:23:31 +0100 wenzelm clarified modules;
less more (0) tip