proper thread context;
authorwenzelm
Mon, 19 Dec 2022 13:28:46 +0100
changeset 76708 2368724cde54
parent 76707 2e231c07b428
child 76709 fdbdc573a06b
proper thread context;
src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 19 13:20:09 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 19 13:28:46 2022 +0100
@@ -56,7 +56,7 @@
   /* global changes */
 
   def state_changed(): Unit = {
-    flush()
+    GUI_Thread.later { flush() }
     PIDE.plugin.deps_changed()
     session.global_options.post(Session.Global_Options(PIDE.options.value))
   }