tuned signature;
authorwenzelm
Sun May 14 20:22:54 2017 +0200 (2017-05-14)
changeset 6583395fd3b9888e6
parent 65832 2fb85623c386
child 65834 67a6e0f166c2
tuned signature;
src/Pure/General/mercurial.scala
src/Pure/General/path.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/General/mercurial.scala	Sun May 14 20:16:13 2017 +0200
     1.2 +++ b/src/Pure/General/mercurial.scala	Sun May 14 20:22:54 2017 +0200
     1.3 @@ -175,9 +175,9 @@
     1.4              case Some(hg) =>
     1.5                val known =
     1.6                  hg.known_files().iterator.map(name =>
     1.7 -                  (hg.root + Path.explode(name)).file.getCanonicalFile).toSet
     1.8 -              if (!known(path.file.getCanonicalFile)) unknown += path
     1.9 -              check(rest.filterNot(p => known(p.file.getCanonicalFile)))
    1.10 +                  (hg.root + Path.explode(name)).canonical_file).toSet
    1.11 +              if (!known(path.canonical_file)) unknown += path
    1.12 +              check(rest.filterNot(p => known(p.canonical_file)))
    1.13            }
    1.14          case Nil =>
    1.15        }
     2.1 --- a/src/Pure/General/path.scala	Sun May 14 20:16:13 2017 +0200
     2.2 +++ b/src/Pure/General/path.scala	Sun May 14 20:22:54 2017 +0200
     2.3 @@ -211,4 +211,6 @@
     2.4    def file: JFile = File.platform_file(this)
     2.5    def is_file: Boolean = file.isFile
     2.6    def is_dir: Boolean = file.isDirectory
     2.7 +
     2.8 +  def canonical_file: JFile = file.getCanonicalFile
     2.9  }
     3.1 --- a/src/Pure/Thy/sessions.scala	Sun May 14 20:16:13 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Sun May 14 20:22:54 2017 +0200
     3.3 @@ -37,9 +37,9 @@
     3.4  
     3.5        def local_theories_iterator =
     3.6        {
     3.7 -        val local_path = local_dir.file.getCanonicalFile.toPath
     3.8 +        val local_path = local_dir.canonical_file.toPath
     3.9          theories.iterator.filter(name =>
    3.10 -          Path.explode(name.node).file.getCanonicalFile.toPath.startsWith(local_path))
    3.11 +          Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
    3.12        }
    3.13  
    3.14        val known_theories =
    3.15 @@ -60,7 +60,7 @@
    3.16          (Map.empty[JFile, List[Document.Node.Name]] /:
    3.17              (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
    3.18            case (known, name) =>
    3.19 -            val file = Path.explode(name.node).file.getCanonicalFile
    3.20 +            val file = Path.explode(name.node).canonical_file
    3.21              val theories1 = known.getOrElse(file, Nil)
    3.22              if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
    3.23                known
     4.1 --- a/src/Pure/Tools/imports.scala	Sun May 14 20:16:13 2017 +0200
     4.2 +++ b/src/Pure/Tools/imports.scala	Sun May 14 20:22:54 2017 +0200
     4.3 @@ -21,7 +21,7 @@
     4.4          progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)")
     4.5          Nil
     4.6        case Some(hg) =>
     4.7 -        val start_path = start.file.getCanonicalFile.toPath
     4.8 +        val start_path = start.canonical_file.toPath
     4.9          for {
    4.10            name <- hg.known_files()
    4.11            file = (hg.root + Path.explode(name)).file
    4.12 @@ -46,7 +46,7 @@
    4.13    {
    4.14      val file =
    4.15        pos match {
    4.16 -        case Position.File(file) => Path.explode(file).file.getCanonicalFile
    4.17 +        case Position.File(file) => Path.explode(file).canonical_file
    4.18          case _ => error("Missing file in position" + Position.here(pos))
    4.19        }
    4.20