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