tuned signature;
authorwenzelm
Sun, 06 Oct 2019 19:33:58 +0200
changeset 70792 ea2834adf8de
parent 70791 02edce6f0c71
child 70793 8ea9b7dec799
child 70794 da647a0c8313
tuned signature;
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)