diff -r 04806ad1e43a -r d8f194556c70 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Dec 28 17:54:55 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 28 19:15:52 2016 +0100
@@ -131,6 +131,12 @@
       }
       else None
     }
+
+    lazy val end_offset: Text.Offset =
+      if (lines.isEmpty) 0
+      else ((0 /: lines) { case (n, line) => n + text_length(line.text) + 1 }) - 1
+
+    def full_range: Text.Range = Text.Range(0, end_offset)
   }