# HG changeset patch # User wenzelm # Date 1670253869 -3600 # Node ID 02d07758ce4280f6f2c27dd7e5bdda171d94c8e3 # Parent 89cd466e063d4ced5079690afd33cf22ec169cbc more robust, notably initial update(); diff -r 89cd466e063d -r 02d07758ce42 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Mon Dec 05 15:41:40 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Mon Dec 05 16:24:29 2022 +0100 @@ -34,19 +34,19 @@ private val syslog = PIDE.session.make_syslog() - private def update(text: String = syslog.content()): Unit = GUI_Thread.require { show(text) } + private def update(text: String = syslog.content()): Unit = show(text) private val delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() } override def echo(msg: String): Unit = { syslog += msg; delay.invoke() } - def load(): Unit = { + 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) } } - update() + GUI_Thread.later { update() } }