changeset 65234 | 1d6e9048cb62 |
parent 65203 | 314246c6eeaa |
child 65522 | 4d7c5df70a14 |
--- a/src/Pure/PIDE/line.scala Tue Mar 14 17:32:19 2017 +0100 +++ b/src/Pure/PIDE/line.scala Tue Mar 14 18:08:21 2017 +0100 @@ -26,6 +26,11 @@ object Position { val zero: Position = Position() + + object Ordering extends scala.math.Ordering[Position] + { + def compare(p1: Position, p2: Position): Int = p1 compare p2 + } } sealed case class Position(line: Int = 0, column: Int = 0)