# HG changeset patch
# User nipkow
# Date 1504634632 -7200
# Node ID a8edca8c4a680ded543a45a69f50cba7d8bbbbf7
# Parent  261dcd52c5a0b4dd79e6b33ec1d2b1f2c0fc0ad1# Parent  f23f044148d308da3a597a047c49a679c6651772
merged

diff -r f23f044148d3 -r a8edca8c4a68 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Tue Sep 05 17:07:42 2017 +0200
+++ b/src/Pure/PIDE/line.scala	Tue Sep 05 20:03:52 2017 +0200
@@ -26,6 +26,7 @@
   object Position
   {
     val zero: Position = Position()
+    val offside: Position = Position(line = -1)
 
     object Ordering extends scala.math.Ordering[Position]
     {
@@ -77,6 +78,11 @@
 
   /* positions within document node */
 
+  object Node_Position
+  {
+    def offside(name: String): Node_Position = Node_Position(name, Position.offside)
+  }
+
   sealed case class Node_Position(name: String, pos: Position = Position.zero)
   {
     def line: Int = pos.line
diff -r f23f044148d3 -r a8edca8c4a68 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Sep 05 17:07:42 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Sep 05 20:03:52 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 {