# HG changeset patch
# User wenzelm
# Date 1483806731 -3600
# Node ID c8bac4b0ef079f983344201f29076a6634c42653
# Parent  37bf7acf6a4bfaf03ad8b03ad933b302ce123e80
tuned;

diff -r 37bf7acf6a4b -r c8bac4b0ef07 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Sat Jan 07 17:30:06 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Sat Jan 07 17:32:11 2017 +0100
@@ -95,16 +95,17 @@
 
   sealed case class Document(lines: List[Line], text_length: Text.Length)
   {
+    lazy val text_range: Text.Range =
+    {
+      val length =
+        if (lines.isEmpty) 0
+        else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
+      Text.Range(0, length)
+    }
     lazy val text: String = lines.mkString("", "\n", "")
     lazy val bytes: Bytes = Bytes(text)
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
 
-    lazy val length: Int =
-      if (lines.isEmpty) 0
-      else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
-
-    def text_range: Text.Range = Text.Range(0, length)
-
     override def toString: String = text
 
     override def equals(that: Any): Boolean =