# HG changeset patch
# User wenzelm
# Date 1743757119 -7200
# Node ID 7fe17f5d15248c776252f7f03068465fff47a320
# Parent  bcbbee58e7e97c07e9617f27502e0b15517cb5a3
tuned signature;

diff -r bcbbee58e7e9 -r 7fe17f5d1524 src/Tools/jEdit/src/isabelle_navigator.scala
--- a/src/Tools/jEdit/src/isabelle_navigator.scala	Fri Apr 04 10:54:37 2025 +0200
+++ b/src/Tools/jEdit/src/isabelle_navigator.scala	Fri Apr 04 10:58:39 2025 +0200
@@ -60,10 +60,6 @@
       }
       else this
     }
-
-    def goto(view: View): Unit = GUI_Thread.require {
-      PIDE.editor.goto_file(true, view, name, offset = offset)
-    }
   }
 
   object History {
@@ -176,7 +172,10 @@
   def goto_current(view: View): Unit = GUI_Thread.require {
     if (_current.defined) {
       val b = _bypass
-      try { _bypass = true; _current.goto(view) }
+      try {
+        _bypass = true
+        PIDE.editor.goto_file(true, view, _current.name, offset = _current.offset)
+      }
       finally { _bypass = b }
     }
   }