src/Tools/jEdit/src/jedit_editor.scala
changeset 66605 261dcd52c5a0
parent 66458 42d0d5c77c78
child 69648 97ddaec3e2ae
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Sep 05 14:29:43 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Sep 05 16:45:23 2017 +0200
@@ -128,7 +128,7 @@
   }
 
   def goto_file(focus: Boolean, view: View, name: String): Unit =
-    goto_file(focus, view, Line.Node_Position(name))
+    goto_file(focus, view, Line.Node_Position.offside(name))
 
   def goto_file(focus: Boolean, view: View, pos: Line.Node_Position)
   {
@@ -215,7 +215,7 @@
     }
 
   def hyperlink_file(focus: Boolean, name: String): Hyperlink =
-    hyperlink_file(focus, Line.Node_Position(name))
+    hyperlink_file(focus, Line.Node_Position.offside(name))
 
   def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
     new Hyperlink {