tuned;
authorwenzelm
Fri, 04 Apr 2025 11:21:01 +0200
changeset 82426 144168941ca4
parent 82425 20f79e12ad20
child 82427 1c646ad68bd8
tuned;
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)
         }
     }
   }