src/Pure/PIDE/line.scala

       line compare that.line match {
         case 0 => column compare that.column
         case i => i
       }
 
-    def advance(text: String, text_length: Length): Position =
+    def advance(text: String, text_length: Text.Length): Position =
       if (text.isEmpty) this
       else {
         val lines = Library.split_lines(text)
         val l = line + lines.length - 1
         val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last))

         case other: Document => lines == other.lines
         case _ => false
       }
     override def hashCode(): Int = lines.hashCode
 
-    def position(text_offset: Text.Offset, text_length: Length): Position =
+    def position(text_offset: Text.Offset, text_length: Text.Length): Position =
     {
       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
       {
         lines_rest match {
           case Nil => require(i == 0); Position(lines_count)

         }
       }
       move(text_offset, 0, lines)
     }
 
-    def range(text_range: Text.Range, text_length: Length): Range =
+    def range(text_range: Text.Range, text_length: Text.Length): Range =
       Range(
         position(text_range.start, text_length),
         position(text_range.stop, text_length))
 
-    def offset(pos: Position, text_length: Length): Option[Text.Offset] =
+    def offset(pos: Position, text_length: Text.Length): Option[Text.Offset] =
     {
       val l = pos.line
       val c = pos.column
       if (0 <= l && l < lines.length) {
         val line_offset =