--- 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() }