src/Tools/VSCode/src/vscode_resources.scala
changeset 64716 473793d52d97
parent 64710 72ca4e5f976e
child 64718 3197b68f4314
--- 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 */