src/Pure/PIDE/document_editor.scala
Mon, 28 Jul 2025 16:10:02 +0200 wenzelm tuned signature;
less more (0) -10 -1 tip