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