src/Tools/VSCode/src/vscode_rendering.scala

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