src/Tools/VSCode/src/vscode_rendering.scala
changeset 65196 e8760a98db78
parent 65176 908d8be90533
child 65213 51c0f094dc02
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 12 13:48:10 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Mar 12 14:23:38 2017 +0100
@@ -200,7 +200,7 @@
           resources.get_file_content(file) match {
             case Some(text) =>
               val chunk = Symbol.Text_Chunk(text)
-              val doc = Line.Document(text, resources.text_length)
+              val doc = Line.Document(text)
               doc.range(chunk.decode(range))
             case _ =>
               Line.Range(Line.Position((line1 - 1) max 0))