# HG changeset patch
# User wenzelm
# Date 1489325489 -3600
# Node ID 8fada74d82bed1003d33a7ff72203541d25f3876
# Parent  e8760a98db7838cd00f55644528278c799bf5ea8
tuned signature;

diff -r e8760a98db78 -r 8fada74d82be src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Sun Mar 12 14:23:38 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Sun Mar 12 14:31:29 2017 +0100
@@ -112,7 +112,9 @@
 
   sealed case class Document(lines: List[Line])
   {
-    lazy val text_range: Text.Range = Text.Range(0, Document.length(lines))
+    lazy val text_length: Text.Offset = Document.length(lines)
+    def text_range: Text.Range = Text.Range(0, text_length)
+
     lazy val text: String = Document.text(lines)
 
     def try_get_text(range: Text.Range): Option[String] =
@@ -160,7 +162,7 @@
         }
         else None
       }
-      else if (l == n && c == 0) Some(text_range.length)
+      else if (l == n && c == 0) Some(text_length)
       else None
     }
 
diff -r e8760a98db78 -r 8fada74d82be src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 14:23:38 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 14:31:29 2017 +0100
@@ -31,6 +31,7 @@
   sealed case class Content(doc: Line.Document)
   {
     override def toString: String = doc.toString
+    def text_length: Text.Offset = doc.text_length
     def text_range: Text.Range = doc.text_range
     def text: String = doc.text
     def try_get_text(range: Text.Range): Option[String] = doc.try_get_text(range)
diff -r e8760a98db78 -r 8fada74d82be src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sun Mar 12 14:23:38 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sun Mar 12 14:31:29 2017 +0100
@@ -312,8 +312,7 @@
         (rendering, offset) <- rendering_offset(node_pos)
         info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1))
       } yield {
-        val doc = rendering.model.content.doc
-        val range = doc.range(info.range)
+        val range = rendering.model.content.doc.range(info.range)
         val contents =
           info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t))))
         (range, contents)
@@ -340,9 +339,9 @@
     val result =
       (for ((rendering, offset) <- rendering_offset(node_pos))
         yield {
-          val doc = rendering.model.content.doc
-          rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.text_range)
-            .map(r => Protocol.DocumentHighlight.text(doc.range(r)))
+          val model = rendering.model
+          rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range)
+            .map(r => Protocol.DocumentHighlight.text(model.content.doc.range(r)))
         }) getOrElse Nil
     channel.write(Protocol.DocumentHighlights.reply(id, result))
   }
diff -r e8760a98db78 -r 8fada74d82be src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 12 14:23:38 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 12 14:31:29 2017 +0100
@@ -286,7 +286,7 @@
       (file, pos) <- st.caret
       model <- st.models.get(file)
       offset <- model.content.doc.offset(pos)
-      if offset < model.content.doc.text_range.stop
+      if offset < model.content.text_length
     }
     yield (model, Text.Range(offset, offset + 1))
   }