equal
deleted
inserted
replaced
111 |
111 |
112 def extract_archive(dir: Path, archive: Path): JDK_Platform = { |
112 def extract_archive(dir: Path, archive: Path): JDK_Platform = { |
113 try { |
113 try { |
114 val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp")) |
114 val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp")) |
115 |
115 |
116 if (archive.get_ext == "zip") { |
116 Isabelle_System.extract(archive, tmp_dir) |
117 Isabelle_System.bash( |
|
118 "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check |
|
119 } |
|
120 else { |
|
121 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check |
|
122 } |
|
123 |
117 |
124 val jdk_dir = File.get_dir(tmp_dir, title = archive.file_name) |
118 val jdk_dir = File.get_dir(tmp_dir, title = archive.file_name) |
125 |
119 |
126 val platform = |
120 val platform = |
127 templates.view.flatMap(_.detect(jdk_dir)) |
121 templates.view.flatMap(_.detect(jdk_dir)) |