--- 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 =>