# HG changeset patch
# User wenzelm
# Date 1743791653 -7200
# Node ID e48b3ddc48101ace028522d0fd96b5be85c106fd
# Parent  96ec907364d75fadb65c55b6ff9c147d37d00762
clarified navigator events: avoid excessive 0 positions;

diff -r 96ec907364d7 -r e48b3ddc4810 src/Tools/jEdit/src/main_plugin.scala
--- 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 _ =>
             }