src/Pure/PIDE/line.scala
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)