# HG changeset patch
# User wenzelm
# Date 1494786174 -7200
# Node ID 95fd3b9888e6ba40453c27bbe1250a3c2a16b89f
# Parent  2fb85623c386fb1c33595ae30ffeb4d9a693d147
tuned signature;

diff -r 2fb85623c386 -r 95fd3b9888e6 src/Pure/General/mercurial.scala
--- 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 =>
       }
diff -r 2fb85623c386 -r 95fd3b9888e6 src/Pure/General/path.scala
--- 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
 }
diff -r 2fb85623c386 -r 95fd3b9888e6 src/Pure/Thy/sessions.scala
--- 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
diff -r 2fb85623c386 -r 95fd3b9888e6 src/Pure/Tools/imports.scala
--- 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))
       }