# HG changeset patch
# User wenzelm
# Date 1743628692 -7200
# Node ID 6898054035d67526ecc8d6f9db1ec4f0c17a3f40
# Parent  9f0f37a12ea8577a351b267af80ff741d7a6e804
support goto_file / hyperlink_file with offset;
clarified signature;

diff -r 9f0f37a12ea8 -r 6898054035d6 src/Tools/jEdit/src/isabelle_navigator.scala
--- a/src/Tools/jEdit/src/isabelle_navigator.scala	Wed Apr 02 23:16:24 2025 +0200
+++ b/src/Tools/jEdit/src/isabelle_navigator.scala	Wed Apr 02 23:18:12 2025 +0200
@@ -62,10 +62,7 @@
     }
 
     def goto(view: View): Unit = GUI_Thread.require {
-      JEdit_Lib.jedit_buffer(name) match {
-        case Some(buffer) => PIDE.editor.goto_buffer(true, view, buffer, offset)
-        case None => PIDE.editor.goto_file(true, view, name)
-      }
+      PIDE.editor.goto_file(true, view, name, offset = offset)
     }
   }
 
diff -r 9f0f37a12ea8 -r 6898054035d6 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 23:16:24 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 23:18:12 2025 +0200
@@ -12,6 +12,7 @@
 
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.browser.VFSBrowser
+import org.gjt.sp.jedit.textarea.TextArea
 import org.gjt.sp.jedit.io.{VFSManager, VFSFile}
 
 
@@ -131,27 +132,30 @@
     }
   }
 
-  def goto_file(focus: Boolean, view: View, name: String): Unit =
-    goto_file(focus, view, Line.Node_Position.offside(name))
-
-  def goto_file(focus: Boolean, view: View, pos: Line.Node_Position): Unit = {
+  def goto_file(
+    focus: Boolean,
+    view: View,
+    name: String,
+    offset: Text.Offset = -1,
+    line: Int = -1,
+    column: Int = -1
+  ): Unit = {
     GUI_Thread.require {}
 
     record_position(view)
 
-    val name = pos.name
-    val line = pos.line
-    val column = pos.column
-
     JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
         if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
         val text_area = view.getTextArea
 
         try {
-          val line_start = text_area.getBuffer.getLineStartOffset(line)
-          text_area.moveCaretPosition(line_start)
-          if (column > 0) text_area.moveCaretPosition(line_start + column)
+          if (offset >= 0) text_area.moveCaretPosition(offset)
+          else if (line >= 0) {
+            val line_start = text_area.getBuffer.getLineStartOffset(line)
+            text_area.moveCaretPosition(line_start)
+            if (column > 0) text_area.moveCaretPosition(line_start + column)
+          }
         }
         catch {
           case _: ArrayIndexOutOfBoundsException =>
@@ -170,7 +174,8 @@
         if (is_dir) VFSBrowser.browseDirectory(view, name)
         else if (!Isabelle_System.open_external_file(name)) {
           val args =
-            if (line <= 0) Array(name)
+            if (offset >= 0) Array(name, "+offset:" + offset)
+            else if (line <= 0) Array(name)
             else if (column <= 0) Array(name, "+line:" + (line + 1))
             else Array(name, "+line:" + (line + 1) + "," + (column + 1))
           jEdit.openFiles(view, null, args)
@@ -210,13 +215,17 @@
       override def toString: String = "URL " + quote(name)
     }
 
-  def hyperlink_file(focus: Boolean, name: String): Hyperlink =
-    hyperlink_file(focus, Line.Node_Position.offside(name))
-
-  def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
+  def hyperlink_file(
+    focus: Boolean,
+    name: String,
+    offset: Text.Offset = -1,
+    line: Int = -1,
+    column: Int = -1
+  ): Hyperlink =
     new Hyperlink {
-      def follow(view: View): Unit = goto_file(focus, view, pos)
-      override def toString: String = "file " + quote(pos.name)
+      def follow(view: View): Unit =
+        goto_file(focus, view, name, offset = offset, line = line, column = column)
+      override def toString: String = "file " + quote(name)
     }
 
   def hyperlink_source_file(
@@ -227,7 +236,7 @@
   ) : Option[Hyperlink] = {
     for (platform_path <- PIDE.resources.source_file(source_name)) yield {
       def hyperlink(pos: Line.Position) =
-        hyperlink_file(focus, Line.Node_Position(platform_path, pos))
+        hyperlink_file(focus, platform_path, line = pos.line, column = pos.column)
 
       if (offset > 0) {
         PIDE.resources.get_file_content(PIDE.resources.node_name(platform_path)) match {
@@ -250,7 +259,10 @@
     offset: Symbol.Offset = 0
   ) : Option[Hyperlink] = {
     if (snapshot.is_outdated) None
-    else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
+    else {
+      snapshot.find_command_position(id, offset)
+        .map(pos => hyperlink_file(focus, pos.name, line = pos.line))
+    }
   }
 
   def is_hyperlink_position(