more robust shutdown of main plugin, while editor continues running;
authorwenzelm
Sat, 23 Aug 2025 21:26:05 +0200
changeset 83045 f6e8930bcf5d
parent 83044 65756f161474
child 83046 8c7599cd6a14
more robust shutdown of main plugin, while editor continues running;
src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Sat Aug 23 13:47:40 2025 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Sat Aug 23 21:26:05 2025 +0200
@@ -45,9 +45,10 @@
 
   @volatile var _plugin: Main_Plugin = null
 
+  def get_plugin: Option[Main_Plugin] = Option(_plugin)
+
   def plugin: Main_Plugin =
-    if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
-    else _plugin
+    get_plugin.getOrElse(error("Uninitialized Isabelle/jEdit plugin"))
 
   def options: JEdit_Options = plugin.options
   def session: JEdit_Session = plugin.session
@@ -482,5 +483,7 @@
     PIDE.editor.shutdown()
 
     Document_Model.reset()
+
+    PIDE._plugin = null
   }
 }