# HG changeset patch
# User wenzelm
# Date 1483179320 -3600
# Node ID 473793d52d976df10839364b644f34a3cde34039
# Parent  33d5fa0ce6e550b9315fbc89caa6490c0a4c4e4e
proper import_name;

diff -r 33d5fa0ce6e5 -r 473793d52d97 src/Tools/VSCode/src/vscode_resources.scala
--- 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 */