--- 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 {