# HG changeset patch
# User wenzelm
# Date 1661024031 -7200
# Node ID 4586e90573acaf96b798dbca4ac6df31dc540e06
# Parent  c14409948063291f493bf6dadde8c777d543f840
more robust GUI initialization (amending 29441f2bfe81);

diff -r c14409948063 -r 4586e90573ac src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Sat Aug 20 21:14:01 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Sat Aug 20 21:33:51 2022 +0200
@@ -300,7 +300,9 @@
   /* resize */
 
   private def handle_resize(): Unit =
-    GUI_Thread.require { operations.foreach(_.pretty_text_area.zoom(zoom)) }
+    GUI_Thread.require {
+      if (operations != null) operations.foreach(_.pretty_text_area.zoom(zoom))
+    }
 
   private val delay_resize =
     Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }