clarified signature: maintan Text.Length within Line.Document;

--- 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

--- a/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 17:10:09 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 17:26:38 2016 +0100
@@ -13,7 +13,7 @@
 
 
 case class Document_Model(
-  session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Text.Length,
+  session: Session, doc: Line.Document, node_name: Document.Node.Name,
   changed: Boolean = true,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
 {

--- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:10:09 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:26:38 2016 +0100
@@ -111,7 +111,7 @@
     for {
       model <- state.value.models.get(node_pos.name)
       rendering = model.rendering(options)
-      offset <- model.doc.offset(node_pos.pos, text_length)
+      offset <- model.doc.offset(node_pos.pos)
     } yield (rendering, offset)
 
 
@@ -134,7 +134,7 @@
     state.change(st =>
       {
         val node_name = resources.node_name(uri)
-        val model = Document_Model(session, Line.Document(text), node_name, text_length)
+        val model = Document_Model(session, Line.Document(text, text_length), node_name)
         st.copy(models = st.models + (uri -> model))
       })
     delay_input.invoke()
@@ -265,7 +265,7 @@
         info <- rendering.tooltip(Text.Range(offset, offset + 1))
       } yield {
         val doc = rendering.model.doc
-        val range = doc.range(info.range, text_length)
+        val range = doc.range(info.range)
         val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
         (range, List("```\n" + s + "\n```"))  // FIXME proper content format
       }

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 17:10:09 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 17:26:38 2016 +0100
@@ -59,7 +59,7 @@
   {
     (for {
       Text.Info(text_range, res) <- results.iterator
-      range = model.doc.range(text_range, model.text_length)
+      range = model.doc.range(text_range)
       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
     } yield {
       val message = Pretty.string_of(body, margin = diagnostics_margin)
@@ -89,10 +89,8 @@
         opt_text match {
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)
-            val doc = Line.Document(text)
-            def position(offset: Symbol.Offset) =
-              doc.position(chunk.decode(offset), model.text_length)
-            Line.Range(position(range.start), position(range.stop))
+            val doc = Line.Document(text, model.doc.text_length)
+            doc.range(chunk.decode(range))
           case _ =>
             Line.Range(Line.Position((line1 - 1) max 0))
         })