diff -r a6d147b22b9b -r 7c23db6b857b src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Mon Jan 16 13:48:03 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Mon Jan 16 20:08:15 2023 +0100
@@ -20,27 +20,6 @@
   }
 
 
-  /* progress */
-
-  class Log_Progress(session: Session) extends Progress {
-    def show(text: String): Unit = {}
-
-    private val syslog = session.make_syslog()
-
-    private def update(text: String = syslog.content()): Unit = show(text)
-    private val delay = Delay.first(session.update_delay, gui = true) { update() }
-
-    override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
-
-    def finish(text: String): Unit = GUI_Thread.require {
-      delay.revoke()
-      update(text)
-    }
-
-    GUI_Thread.later { update() }
-  }
-
-
   /* configuration state */
 
   sealed case class State(