more robust (amending 4ca84abb16ef): Main_Plugin.start() could happen on other thread, e.g. when $JEDIT_SETTINGS/recent.xml refers to "isabelle-export:" URL;
--- 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))
}