# HG changeset patch
# User wenzelm
# Date 1746957910 -7200
# Node ID bfc920530ae6bbf1ac71cc07bdc4ffad09acebdf
# Parent  5bd33fa698c74f5d71583783e2b5cc99d0c7821c
more robust (amending 4ca84abb16ef): Main_Plugin.start() could happen on other thread, e.g. when $JEDIT_SETTINGS/recent.xml refers to "isabelle-export:" URL;

diff -r 5bd33fa698c7 -r bfc920530ae6 src/Tools/jEdit/src/isabelle_navigator.scala
--- a/src/Tools/jEdit/src/isabelle_navigator.scala	Fri May 09 14:15:10 2025 +0200
+++ b/src/Tools/jEdit/src/isabelle_navigator.scala	Sun May 11 12:05:10 2025 +0200
@@ -147,12 +147,12 @@
   private val buffer_listener =
     JEdit_Lib.buffer_listener((buffer, edit) => convert(JEdit_Lib.buffer_name(buffer), edit))
 
-  def exit(buffers: IterableOnce[Buffer]): Unit = GUI_Thread.require {
+  def exit(buffers: IterableOnce[Buffer]): Unit = GUI_Thread.later {
     buffers.iterator.foreach(_.removeBufferListener(buffer_listener))
     close(buffers.iterator.map(JEdit_Lib.buffer_name).toSet)
   }
 
-  def init(buffers: IterableOnce[Buffer]): Unit = GUI_Thread.require {
+  def init(buffers: IterableOnce[Buffer]): Unit = GUI_Thread.later {
     exit(buffers)
     buffers.iterator.foreach(_.addBufferListener(buffer_listener))
   }