# HG changeset patch
# User wenzelm
# Date 1742914434 -3600
# Node ID 47c4ea946fc8cb1fe68b9fa5ae6b36bec0c598c0
# Parent  6e80327eb30ac0d211014e0f0dbae888c1e01e88
more robust;

diff -r 6e80327eb30a -r 47c4ea946fc8 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Tue Mar 25 15:50:41 2025 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Mar 25 15:53:54 2025 +0100
@@ -312,10 +312,12 @@
           jEdit.propertiesChanged()
 
           val view = jEdit.getActiveView
-          init_editor(view)
+          if (view != null) {
+            init_editor(view)
 
-          PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
-            JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
+            PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
+              JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
+          }
 
         case msg: ViewUpdate
         if msg.getWhat == ViewUpdate.CREATED && msg.getView != null =>