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