--- 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() }