src/Tools/VSCode/src/vscode_rendering.scala
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)