# HG changeset patch
# User wenzelm
# Date 1671452926 -3600
# Node ID 2368724cde54ab430a344fb2d546f467d11abfce
# Parent  2e231c07b4280c902dc25c7ea42fb127b369f44d
proper thread context;

diff -r 2e231c07b428 -r 2368724cde54 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))
   }