--- a/src/Tools/jEdit/src/state_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -40,7 +40,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }