# 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 */