# HG changeset patch
# User wenzelm
# Date 1483449423 -3600
# Node ID 100941134718c7de39e0687a67c7ee0aa5484d79
# Parent  7e3924224769346df21d06eed2a14884fd0d2a31
clarified master_dir: file-URL;

diff -r 7e3924224769 -r 100941134718 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Jan 02 18:08:04 2017 +0100
+++ b/src/Pure/General/file.scala	Tue Jan 03 14:17:03 2017 +0100
@@ -48,6 +48,7 @@
   def standard_path(file: JFile): String = standard_path(file.getPath)
 
   def path(file: JFile): Path = Path.explode(standard_path(file))
+  def pwd(): Path = path(Path.current.file.toPath.toAbsolutePath.toFile)
 
   def standard_url(name: String): String =
     try {
diff -r 7e3924224769 -r 100941134718 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Mon Jan 02 18:08:04 2017 +0100
+++ b/src/Pure/General/url.scala	Tue Jan 03 14:17:03 2017 +0100
@@ -57,6 +57,19 @@
     try { file(uri); true }
     catch { case _: URISyntaxException | _: IllegalArgumentException => false }
 
+  def normalize_file(uri: String): String =
+    if (is_wellformed_file(uri)) {
+      val uri1 = new URI(uri).normalize.toASCIIString
+      if (uri1.startsWith("file://")) uri1
+      else {
+        Library.try_unprefix("file:/", uri1) match {
+          case Some(p) => "file:///" + p
+          case None => uri1
+        }
+      }
+    }
+    else uri
+
   def platform_file(path: Path): String =
   {
     val path1 = path.expand
diff -r 7e3924224769 -r 100941134718 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Jan 02 18:08:04 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Jan 03 14:17:03 2017 +0100
@@ -48,10 +48,6 @@
     if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name))
     else raw_name
 
-  def append_file_url(dir: String, raw_name: String): String =
-    if (Path.is_valid(raw_name)) "file://" + append(dir, Path.explode(raw_name))
-    else raw_name
-
 
 
   /* source files of Isabelle/ML bootstrap */
diff -r 7e3924224769 -r 100941134718 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Jan 02 18:08:04 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Tue Jan 03 14:17:03 2017 +0100
@@ -77,9 +77,13 @@
   val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
 
+  private val Dir_Name = new Regex("""(.*?)[^/\\:]+""")
   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
 
+  def dir_name(s: String): String =
+    s match { case Dir_Name(name) => name case _ => "" }
+
   def base_name(s: String): String =
     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
 
diff -r 7e3924224769 -r 100941134718 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Jan 02 18:08:04 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jan 03 14:17:03 2017 +0100
@@ -126,7 +126,7 @@
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
-            val file = resources.append_file_url(snapshot.node_name.master_dir, name)
+            val file = resources.append_file(snapshot.node_name.master_dir, name)
             Some(Line.Node_Range(file) :: links)
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
diff -r 7e3924224769 -r 100941134718 src/Tools/VSCode/src/vscode_resources.scala
--- 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 =