src/Pure/PIDE/document_editor.scala
changeset 76732 0ba6f360d38a
parent 76730 1b8dd8c0492f
child 76739 cb72b5996520
--- a/src/Pure/PIDE/document_editor.scala	Wed Dec 21 14:14:02 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Wed Dec 21 15:34:33 2022 +0100
@@ -32,10 +32,9 @@
 
     override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
 
-    def load(): Unit = GUI_Thread.require {
-      val path = document_output().log
-      val text = if (path.is_file) File.read(path) else ""
-      GUI_Thread.later { delay.revoke(); update(text) }
+    def finish(text: String): Unit = GUI_Thread.require {
+      delay.revoke()
+      update(text)
     }
 
     GUI_Thread.later { update() }