equal
deleted
inserted
replaced
144 |
144 |
145 |
145 |
146 /** skeleton for component **/ |
146 /** skeleton for component **/ |
147 |
147 |
148 private def extract_sources(source_archive: Path, component_dir: Path): Unit = { |
148 private def extract_sources(source_archive: Path, component_dir: Path): Unit = { |
149 if (source_archive.get_ext == "zip") { |
149 Isabelle_System.extract(source_archive, component_dir) |
150 Isabelle_System.bash( |
|
151 "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check |
|
152 } |
|
153 else { |
|
154 Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check |
|
155 } |
|
156 |
150 |
157 val src_dir = component_dir + Path.explode("src") |
151 val src_dir = component_dir + Path.explode("src") |
158 File.read_dir(component_dir) match { |
152 File.read_dir(component_dir) match { |
159 case List(s) => Isabelle_System.move_file(component_dir + Path.basic(s), src_dir) |
153 case List(s) => Isabelle_System.move_file(component_dir + Path.basic(s), src_dir) |
160 case _ => error("Source archive contains multiple directories") |
154 case _ => error("Source archive contains multiple directories") |