changeset 64706 | 3ebf9f8299df |
parent 64704 | 08c2d80428ff |
child 64730 | 76996d915894 |
--- 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))