# HG changeset patch
# User wenzelm
# Date 1743593952 -7200
# Node ID a6046b6d23b46774a5a2883f9fb0f9716caa3150
# Parent  6ea8b99cd8d4eecc676af6b6698a22f8049da385
more accurate navigator position;

diff -r 6ea8b99cd8d4 -r a6046b6d23b4 src/Tools/jEdit/src/isabelle_navigator.scala
--- a/src/Tools/jEdit/src/isabelle_navigator.scala	Tue Apr 01 21:37:02 2025 +0200
+++ b/src/Tools/jEdit/src/isabelle_navigator.scala	Wed Apr 02 13:39:12 2025 +0200
@@ -180,6 +180,7 @@
 
   def record(buffer: Buffer): Unit = record(Pos(buffer))
   def record(edit_pane: EditPane): Unit = record(Pos(edit_pane))
+  def record(view: View): Unit = record(Pos(view))
 
   def goto_current(view: View): Unit = GUI_Thread.require {
     if (_current.defined) {
diff -r 6ea8b99cd8d4 -r a6046b6d23b4 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 01 21:37:02 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 13:39:12 2025 +0200
@@ -109,7 +109,8 @@
 
   /* navigation */
 
-  def push_position(view: View): Unit = {
+  def record_position(view: View): Unit = {
+    PIDE.plugin.navigator.record(view)
     val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
     if (navigator != null) {
       try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
@@ -120,7 +121,7 @@
   def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset): Unit = {
     GUI_Thread.require {}
 
-    push_position(view)
+    record_position(view)
 
     if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
     try { view.getTextArea.moveCaretPosition(offset) }
@@ -136,7 +137,7 @@
   def goto_file(focus: Boolean, view: View, pos: Line.Node_Position): Unit = {
     GUI_Thread.require {}
 
-    push_position(view)
+    record_position(view)
 
     val name = pos.name
     val line = pos.line
diff -r 6ea8b99cd8d4 -r a6046b6d23b4 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Tue Apr 01 21:37:02 2025 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Wed Apr 02 13:39:12 2025 +0200
@@ -379,16 +379,7 @@
             if (what == EditPaneUpdate.DESTROYED) Completion_Popup.Text_Area.exit(text_area)
           }
 
-          msg match {
-            case m: BufferChanging =>
-              val new_buffer = m.getBuffer
-              if (new_buffer != null && !new_buffer.isUntitled) {
-                if (edit_pane == null) navigator.record(new_buffer)
-                else navigator.record(edit_pane)
-              }
-            case _: PositionChanging => navigator.record(edit_pane)
-            case _ =>
-          }
+          if (msg.isInstanceOf[PositionChanging]) navigator.record(edit_pane)
 
         case _: PropertiesChanged =>
           for {