src/Pure/PIDE/line.scala

--- a/src/Pure/PIDE/line.scala	Sun Oct 06 16:25:20 2019 +0200
+++ b/src/Pure/PIDE/line.scala	Sun Oct 06 19:33:58 2019 +0200
@@ -86,7 +86,9 @@
   sealed case class Node_Position(name: String, pos: Position = Position.zero)
   {
     def line: Int = pos.line
+    def line1: Int = pos.line1
     def column: Int = pos.column
+    def column1: Int = pos.column1
   }
 
   sealed case class Node_Range(name: String, range: Range = Range.zero)