--- a/src/Pure/General/url.scala Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Pure/General/url.scala Fri Jun 30 14:19:37 2017 +0200
@@ -49,7 +49,7 @@
/* file URIs */
- def print_file(file: JFile): String = file.toPath.toAbsolutePath.toUri.normalize.toString
+ def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString
def print_file_name(name: String): String = print_file(new JFile(name))
def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
@@ -61,6 +61,6 @@
false
}
- def canonical_file(uri: String): JFile = parse_file(uri).getCanonicalFile
+ def canonical_file(uri: String): JFile = File.canonical(parse_file(uri))
def canonical_file_name(uri: String): String = canonical_file(uri).getPath
}
--- a/src/Pure/Thy/sessions.scala Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Jun 30 14:19:37 2017 +0200
@@ -83,7 +83,7 @@
def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
{
- val res = files.getOrElse(file.getCanonicalFile, Nil).headOption
+ val res = files.getOrElse(File.canonical(file), Nil).headOption
if (bootstrap) res.map(_.map_theory(Thy_Header.bootstrap_name(_))) else res
}
}
--- a/src/Pure/Tools/imports.scala Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Pure/Tools/imports.scala Fri Jun 30 14:19:37 2017 +0200
@@ -25,7 +25,7 @@
for {
name <- hg.known_files()
file = (hg.root + Path.explode(name)).file
- if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path)
+ if pred(file) && File.canonical(file).toPath.startsWith(start_path)
} yield file
}
--- a/src/Tools/VSCode/src/vscode_rendering.scala Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Jun 30 14:19:37 2017 +0200
@@ -254,7 +254,7 @@
for {
platform_path <- resources.source_file(source_name)
file <-
- (try { Some(new JFile(platform_path).getCanonicalFile) }
+ (try { Some(File.canonical(new JFile(platform_path))) }
catch { case ERROR(_) => None })
}
yield {
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Jun 30 14:19:37 2017 +0200
@@ -109,7 +109,7 @@
else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
dir + JFile.separator + File.platform_path(path)
else if (path.is_basic) dir + File.platform_path(path)
- else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
+ else File.canonical_name(new JFile(dir + JFile.separator + File.platform_path(path)))
}
def get_models: Map[JFile, Document_Model] = state.value.models
--- a/src/Tools/jEdit/src/scala_console.scala Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Fri Jun 30 14:19:37 2017 +0200
@@ -30,7 +30,7 @@
def find_jars(start: String): List[String] =
if (start != null)
File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
- map(_.getAbsolutePath)
+ map(File.absolute_name(_))
else Nil
val initial_class_path =