--- a/src/Tools/VSCode/src/vscode_resources.scala Sat Dec 31 08:12:31 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Dec 31 11:15:20 2016 +0100
@@ -55,6 +55,14 @@
Document.Node.Name(uri, master_dir, theory)
}
+ override def import_name(qualifier: String, master: Document.Node.Name, s: String)
+ : Document.Node.Name =
+ {
+ val name = super.import_name(qualifier, master, s)
+ if (name.node.startsWith("file://") || name.node.forall(c => c != '/' && c != '\\')) name
+ else name.copy(node = "file://" + name.node)
+ }
+
/* document models */