diff -r e37209c0a42a -r 1d6e9048cb62 src/Pure/PIDE/line.scala
--- 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)