clarified navigator events: avoid excessive 0 positions;

--- a/src/Tools/jEdit/src/main_plugin.scala	Fri Apr 04 20:31:57 2025 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Fri Apr 04 20:34:13 2025 +0200
@@ -348,11 +348,6 @@
           if (buffer != null && !buffer.isUntitled) {
             what match {
               case BufferUpdate.CREATED => navigator.init(Set(buffer))
-              case BufferUpdate.LOADED =>
-                if (view_edit_pane != null && view_edit_pane.getBuffer == buffer) {
-                  navigator.record(view_edit_pane)
-                }
-                else navigator.record(buffer)
               case BufferUpdate.CLOSED => navigator.exit(Set(buffer))
               case _ =>
             }