--- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Jan 04 15:20:54 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Jan 04 19:42:08 2017 +0100
@@ -84,11 +84,11 @@
if Path.is_wellformed(name)
}
yield {
- val file = Path.explode(name).file
+ val path = Path.explode(name)
val opt_text =
- try { Some(File.read(file)) } // FIXME content from resources/models
+ try { Some(File.read(path)) } // FIXME content from resources/models
catch { case ERROR(_) => None }
- Line.Node_Range(Url.print_file(file),
+ Line.Node_Range(File.platform_path(path),
opt_text match {
case Some(text) if range.start > 0 =>
val chunk = Symbol.Text_Chunk(text)