# HG changeset patch
# User wenzelm
# Date 1483023629 -3600
# Node ID 931f51fb24ca94803675d26d5f5aac1971379480
# Parent  14deaeaa6476b13e921ea6ca9f37653b78a7e842
clarified Document.length -- independent of text_length;

diff -r 14deaeaa6476 -r 931f51fb24ca src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Thu Dec 29 15:37:15 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Thu Dec 29 16:00:29 2016 +0100
@@ -132,11 +132,11 @@
       else None
     }
 
-    lazy val end_offset: Text.Offset =
+    lazy val length: Int =
       if (lines.isEmpty) 0
-      else ((0 /: lines) { case (n, line) => n + text_length(line.text) + 1 }) - 1
+      else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
 
-    def full_range: Text.Range = Text.Range(0, end_offset)
+    def full_range: Text.Range = Text.Range(0, length)
   }