# HG changeset patch
# User wenzelm
# Date 1743628979 -7200
# Node ID 955c5d6c1acf7574da8a385720be0deb94789b0b
# Parent  6898054035d67526ecc8d6f9db1ec4f0c17a3f40
remove goto_buffer in favour of uniform goto_file;

diff -r 6898054035d6 -r 955c5d6c1acf src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Apr 02 23:18:12 2025 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Apr 02 23:22:59 2025 +0200
@@ -569,7 +569,8 @@
       val errs = rendering.errors(range).filterNot(_.range.overlaps(avoid_range))
       get(errs) match {
         case Some(err) =>
-          PIDE.editor.goto_buffer(false, view, view.getBuffer, err.range.start)
+          PIDE.editor.goto_file(
+            false, view, JEdit_Lib.buffer_name(view.getBuffer), offset = err.range.start)
         case None =>
           view.getStatus.setMessageAndClear("No " + which + "error in current document snapshot")
       }
diff -r 6898054035d6 -r 955c5d6c1acf src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 23:18:12 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 23:22:59 2025 +0200
@@ -110,28 +110,6 @@
 
   /* navigation */
 
-  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) }
-      catch { case _: NoSuchMethodException => }
-    }
-  }
-
-  def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset): Unit = {
-    GUI_Thread.require {}
-
-    record_position(view)
-
-    if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
-    try { view.getTextArea.moveCaretPosition(offset) }
-    catch {
-      case _: ArrayIndexOutOfBoundsException =>
-      case _: IllegalArgumentException =>
-    }
-  }
-
   def goto_file(
     focus: Boolean,
     view: View,
@@ -142,7 +120,12 @@
   ): Unit = {
     GUI_Thread.require {}
 
-    record_position(view)
+    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) }
+      catch { case _: NoSuchMethodException => }
+    }
 
     JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>