src/Pure/PIDE/document_editor.scala
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