src/Pure/Admin/build_jdk.scala
changeset 73086 178c9d04e08c
parent 73084 4f1df8d3707b
child 73087 198fe1e7ed32
equal deleted inserted replaced
73085:b595bcdf5bf3 73086:178c9d04e08c
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
       
    10 import java.io.{File => JFile}
    10 import java.nio.file.Files
    11 import java.nio.file.Files
    11 import java.nio.file.attribute.PosixFilePermission
    12 import java.nio.file.attribute.PosixFilePermission
    12 
    13 
    13 import scala.util.matching.Regex
    14 import scala.util.matching.Regex
    14 
    15 
   199           }
   200           }
   200           Files.setPosixFilePermissions(path, perms)
   201           Files.setPosixFilePermissions(path, perms)
   201         }
   202         }
   202 
   203 
   203         progress.echo("Sharing ...")
   204         progress.echo("Sharing ...")
   204         val main_dir :: other_dirs =
   205         val all_files: Multi_Map[SHA1.Digest, JFile] =
   205           platforms.map(platform => (component_dir + platform.platform_path).file.toPath)
   206           (Multi_Map.empty[SHA1.Digest, JFile] /:
   206         for {
   207             File.find_files(component_dir.file, file => Files.isSymbolicLink(file.toPath)))
   207           file1 <- File.find_files(main_dir.toFile).iterator
   208           {
   208           path1 = file1.toPath
   209             case (seen, file) =>
   209           dir2 <- other_dirs.iterator
   210               val digest = SHA1.digest(Bytes.read(file))
   210         } {
   211               seen.insert(digest, file)
   211           val path2 = dir2.resolve(main_dir.relativize(path1))
   212           }
   212           val file2 = path2.toFile
   213         for ((_, file1 :: files2) <- all_files.iterator_list; file2 <- files2) {
   213           if (!Files.isSymbolicLink(path2) && file2.isFile && File.eq_content(file1, file2)) {
   214           if (file2.isFile && File.eq_content(file1, file2)) {
   214             file2.delete
   215             file2.delete
   215             Files.createLink(path2, path1)
   216             progress.echo(file1 + " -> " + file2)
       
   217             Files.createLink(file2.toPath, file1.toPath)
   216           }
   218           }
   217         }
   219         }
   218 
   220 
   219         progress.echo("Archiving ...")
   221         progress.echo("Archiving ...")
   220         Isabelle_System.gnutar(
   222         Isabelle_System.gnutar(