src/Tools/VSCode/src/vscode_rendering.scala
changeset 69261 c78c95d2a3d1
parent 67824 661cd25304ae
child 70079 990c6e8faf2c
     1.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Nov 07 21:42:16 2018 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Nov 07 22:15:03 2018 +0100
     1.3 @@ -264,7 +264,7 @@
     1.4      yield {
     1.5        Line.Node_Range(file.getPath,
     1.6          if (range.start > 0) {
     1.7 -          resources.get_file_content(file) match {
     1.8 +          resources.get_file_content(resources.node_name(file)) match {
     1.9              case Some(text) =>
    1.10                val chunk = Symbol.Text_Chunk(text)
    1.11                val doc = Line.Document(text)