changeset 64668 | 39a6c88c059b |
parent 64667 | cdb0d559a24b |
child 64679 | b2bf280b7e13 |
--- a/src/Tools/VSCode/src/vscode_rendering.scala Fri Dec 23 19:19:59 2016 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Dec 23 20:06:54 2016 +0100 @@ -40,7 +40,7 @@ val opt_text = try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models catch { case ERROR(_) => None } - Line.Node_Range(name, + Line.Node_Range(File.platform_url(name), opt_text match { case Some(text) if range.start > 0 => val chunk = Symbol.Text_Chunk(text)