more robust (amending 4ca84abb16ef): Main_Plugin.start() could happen on other thread, e.g. when $JEDIT_SETTINGS/recent.xml refers to "isabelle-export:" URL; default tip
authorwenzelm
Sun, 11 May 2025 12:05:10 +0200
changeset 82619 bfc920530ae6
parent 82618 5bd33fa698c7
more robust (amending 4ca84abb16ef): Main_Plugin.start() could happen on other thread, e.g. when $JEDIT_SETTINGS/recent.xml refers to "isabelle-export:" URL;
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))
   }