--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Jan 02 18:08:04 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Jan 03 14:17:03 2017 +0100
@@ -43,16 +43,17 @@
val theory = Thy_Header.thy_name_bootstrap(uri).getOrElse("")
val master_dir =
if (!Url.is_wellformed_file(uri) || theory == "") ""
- else Url.file(uri).getCanonicalFile.getParent
+ else Thy_Header.dir_name(uri)
Document.Node.Name(uri, master_dir, theory)
}
- override def import_name(qualifier: String, master: Document.Node.Name, s: String)
- : Document.Node.Name =
+ override def append(dir: String, source_path: Path): String =
{
- 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)
+ val path = source_path.expand
+ if (path.is_absolute) "file://" + path.implode
+ else if (dir == "") "file://" + (File.pwd() + path).implode
+ else if (path.is_current) dir
+ else Url.normalize_file(dir + "/" + path.implode)
}
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =