# HG changeset patch
# User wenzelm
# Date 1504622723 -7200
# Node ID 261dcd52c5a0b4dd79e6b33ec1d2b1f2c0fc0ad1
# Parent  1af360d1cad257a3302621ee9f9bed14d4476c96
less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);

diff -r 1af360d1cad2 -r 261dcd52c5a0 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Tue Sep 05 14:29:43 2017 +0200
+++ b/src/Pure/PIDE/line.scala	Tue Sep 05 16:45:23 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 1af360d1cad2 -r 261dcd52c5a0 src/Tools/jEdit/src/jedit_editor.scala
--- 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 {