# HG changeset patch
# User wenzelm
# Date 1483559526 -3600
# Node ID 7884a19de32505027b4b12d93fbf3a184a9fe9b3
# Parent  ca09695eb43c81855bdaf8e8af0dd6ece6fd4744
proper interpretation of Resources.source_file as platform file;

diff -r ca09695eb43c -r 7884a19de325 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jan 04 19:42:08 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jan 04 20:52:06 2017 +0100
@@ -10,6 +10,9 @@
 
 import isabelle._
 
+import java.io.{File => JFile}
+
+
 object VSCode_Rendering
 {
   /* diagnostic messages */
@@ -81,14 +84,15 @@
   {
     for {
       name <- resources.source_file(source_name)
-      if Path.is_wellformed(name)
+      file <-
+        (try { Some(new JFile(name).getCanonicalFile) }
+         catch { case ERROR(_) => None })
     }
     yield {
-      val path = Path.explode(name)
       val opt_text =
-        try { Some(File.read(path)) } // FIXME content from resources/models
+        try { Some(File.read(file)) } // FIXME content from resources/models
         catch { case ERROR(_) => None }
-      Line.Node_Range(File.platform_path(path),
+      Line.Node_Range(file.getPath,
         opt_text match {
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)