more robust;
authorwenzelm
Tue, 25 Mar 2025 15:53:54 +0100
changeset 82404 47c4ea946fc8
parent 82403 6e80327eb30a
child 82405 f3fbe96bd718
more robust;
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 =>