# HG changeset patch
# User wenzelm
# Date 1743758461 -7200
# Node ID 144168941ca415c5da8292a42aa3f6e62b28ad5e
# Parent  20f79e12ad207818a7c6d5069a7d4116ae0d7c0a
tuned;

diff -r 20f79e12ad20 -r 144168941ca4 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 11:00:06 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 11:21:01 2025 +0200
@@ -151,12 +151,13 @@
 
         if (is_dir) VFSBrowser.browseDirectory(view, name)
         else if (!Isabelle_System.open_external_file(name)) {
-          val args =
-            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)
+          val marker =
+            if (offset >= 0) "+offset:" + offset
+            else if (line <= 0) ""
+            else if (column <= 0) "+line:" + (line + 1)
+            else "+line:" + (line + 1) + "," + (column + 1)
+          val buffer = jEdit.openFile(view, name)
+          if (buffer != null && marker.nonEmpty) jEdit.gotoMarker(view, buffer, marker)
         }
     }
   }