--- a/src/Tools/jEdit/src/monitor_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -59,10 +59,10 @@
}
private val input_delay =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_input_delay")) { update_chart }
+ Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart }
private val update_delay =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
+ Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart }
/* controls */