--- a/src/Pure/General/mercurial.scala Sun May 14 20:16:13 2017 +0200
+++ b/src/Pure/General/mercurial.scala Sun May 14 20:22:54 2017 +0200
@@ -175,9 +175,9 @@
case Some(hg) =>
val known =
hg.known_files().iterator.map(name =>
- (hg.root + Path.explode(name)).file.getCanonicalFile).toSet
- if (!known(path.file.getCanonicalFile)) unknown += path
- check(rest.filterNot(p => known(p.file.getCanonicalFile)))
+ (hg.root + Path.explode(name)).canonical_file).toSet
+ if (!known(path.canonical_file)) unknown += path
+ check(rest.filterNot(p => known(p.canonical_file)))
}
case Nil =>
}
--- a/src/Pure/General/path.scala Sun May 14 20:16:13 2017 +0200
+++ b/src/Pure/General/path.scala Sun May 14 20:22:54 2017 +0200
@@ -211,4 +211,6 @@
def file: JFile = File.platform_file(this)
def is_file: Boolean = file.isFile
def is_dir: Boolean = file.isDirectory
+
+ def canonical_file: JFile = file.getCanonicalFile
}
--- a/src/Pure/Thy/sessions.scala Sun May 14 20:16:13 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Sun May 14 20:22:54 2017 +0200
@@ -37,9 +37,9 @@
def local_theories_iterator =
{
- val local_path = local_dir.file.getCanonicalFile.toPath
+ val local_path = local_dir.canonical_file.toPath
theories.iterator.filter(name =>
- Path.explode(name.node).file.getCanonicalFile.toPath.startsWith(local_path))
+ Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
}
val known_theories =
@@ -60,7 +60,7 @@
(Map.empty[JFile, List[Document.Node.Name]] /:
(bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
case (known, name) =>
- val file = Path.explode(name.node).file.getCanonicalFile
+ val file = Path.explode(name.node).canonical_file
val theories1 = known.getOrElse(file, Nil)
if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
known
--- a/src/Pure/Tools/imports.scala Sun May 14 20:16:13 2017 +0200
+++ b/src/Pure/Tools/imports.scala Sun May 14 20:22:54 2017 +0200
@@ -21,7 +21,7 @@
progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)")
Nil
case Some(hg) =>
- val start_path = start.file.getCanonicalFile.toPath
+ val start_path = start.canonical_file.toPath
for {
name <- hg.known_files()
file = (hg.root + Path.explode(name)).file
@@ -46,7 +46,7 @@
{
val file =
pos match {
- case Position.File(file) => Path.explode(file).file.getCanonicalFile
+ case Position.File(file) => Path.explode(file).canonical_file
case _ => error("Missing file in position" + Position.here(pos))
}