src/Pure/PIDE/line.scala

--- a/src/Pure/PIDE/line.scala	Wed Dec 28 17:10:09 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 28 17:26:38 2016 +0100
@@ -80,21 +80,14 @@
 
   object Document
   {
-    val empty: Document = new Document(Nil)
-
-    def apply(lines: List[Line]): Document =
-      if (lines.isEmpty) empty
-      else new Document(lines)
-
-    def apply(text: String): Document =
-      if (text == "") empty
-      else if (text.contains('\r'))
-        new Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))))
+    def apply(text: String, text_length: Text.Length): Document =
+      if (text.contains('\r'))
+        Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))), text_length)
       else
-        new Document(Library.split_lines(text).map(s => Line(s)))
+        Document(Library.split_lines(text).map(s => Line(s)), text_length)
   }
 
-  final class Document private(val lines: List[Line])
+  sealed case class Document(lines: List[Line], text_length: Text.Length)
   {
     def make_text: String = lines.mkString("", "\n", "")
 
@@ -107,7 +100,7 @@
       }
     override def hashCode(): Int = lines.hashCode
 
-    def position(text_offset: Text.Offset, text_length: Text.Length): Position =
+    def position(text_offset: Text.Offset): Position =
     {
       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
       {
@@ -123,12 +116,10 @@
       move(text_offset, 0, lines)
     }
 
-    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 range(text_range: Text.Range): Range =
+      Range(position(text_range.start), position(text_range.stop))
 
-    def offset(pos: Position, text_length: Text.Length): Option[Text.Offset] =
+    def offset(pos: Position): Option[Text.Offset] =
     {
       val l = pos.line
       val c = pos.column