changeset 64730 | 76996d915894 |
parent 64706 | 3ebf9f8299df |
child 64759 | 100941134718 |
--- a/src/Tools/VSCode/src/vscode_rendering.scala Sun Jan 01 11:38:29 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sun Jan 01 11:47:27 2017 +0100 @@ -84,7 +84,7 @@ val opt_text = try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models catch { case ERROR(_) => None } - Line.Node_Range(File.platform_url(name), + Line.Node_Range(Url.platform_file(name), opt_text match { case Some(text) if range.start > 0 => val chunk = Symbol.Text_Chunk(text)