src/Pure/PIDE/line.scala

     def text(lines: List[Line]): String = lines.mkString("", "\n", "")
   }
 
   sealed case class Document(lines: List[Line])
   {
-    lazy val text_range: Text.Range = Text.Range(0, Document.length(lines))
+    lazy val text_length: Text.Offset = Document.length(lines)
+    def text_range: Text.Range = Text.Range(0, text_length)
+
     lazy val text: String = Document.text(lines)
 
     def try_get_text(range: Text.Range): Option[String] =
       if (text_range.contains(range)) Some(text.substring(range.start, range.stop))
       else None

             (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 }
           Some(line_offset + c)
         }
         else None
       }
-      else if (l == n && c == 0) Some(text_range.length)
+      else if (l == n && c == 0) Some(text_length)
       else None
     }
 
     def change(remove: Range, insert: String): Option[(List[Text.Edit], Document)] =
     {