--- 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 {
--- 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
--- 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 */
--- 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)) }
--- 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), _))) =>
--- 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 =