--- a/src/Tools/jEdit/src/syslog_dockable.scala Thu Dec 08 22:11:36 2022 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Thu Dec 08 22:38:03 2022 +0100
@@ -19,10 +19,11 @@
private val syslog = new TextArea()
- private def syslog_delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
- val text = PIDE.session.syslog.content()
- if (text != syslog.text) syslog.text = text
- }
+ private def syslog_delay =
+ Delay.first(PIDE.session.update_delay, gui = true) {
+ val text = PIDE.session.syslog.content()
+ if (text != syslog.text) syslog.text = text
+ }
set_content(new ScrollPane(syslog))