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