# HG changeset patch
# User wenzelm
# Date 1483089970 -3600
# Node ID 3ebf9f8299df3c15f53f9c0170457521eeb95939
# Parent  08c2d80428ff7922599e4f209f43a0989ab2e851
tuned;

diff -r 08c2d80428ff -r 3ebf9f8299df src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Dec 29 22:10:29 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 10:26:10 2016 +0100
@@ -165,7 +165,7 @@
         val content = Build.session_content(options, false, session_dirs, session_name)
         val resources =
           new VSCode_Resources(
-            options, content.loaded_theories, content.known_theories, content.syntax)
+            options, text_length, content.loaded_theories, content.known_theories, content.syntax)
 
         Some(new Session(resources) {
           override def output_delay = options.seconds("editor_output_delay")
diff -r 08c2d80428ff -r 3ebf9f8299df src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Thu Dec 29 22:10:29 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 30 10:26:10 2016 +0100
@@ -88,7 +88,7 @@
         opt_text match {
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)
-            val doc = Line.Document(text, model.doc.text_length)
+            val doc = Line.Document(text, resources.text_length)
             doc.range(chunk.decode(range))
           case _ =>
             Line.Range(Line.Position((line1 - 1) max 0))
diff -r 08c2d80428ff -r 3ebf9f8299df src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Dec 29 22:10:29 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 10:26:10 2016 +0100
@@ -35,6 +35,7 @@
 
 class VSCode_Resources(
     val options: Options,
+    val text_length: Text.Length,
     loaded_theories: Set[String],
     known_theories: Map[String, Document.Node.Name],
     base_syntax: Outer_Syntax)