equal
deleted
inserted
replaced
62 ): Unit = { |
62 ): Unit = { |
63 /* component */ |
63 /* component */ |
64 |
64 |
65 val component_name = main_download.name + "-" + main_download.version |
65 val component_name = main_download.name + "-" + main_download.version |
66 val component_dir = |
66 val component_dir = |
67 Components.Directory.create(target_dir + Path.basic(component_name), progress = progress) |
67 Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress) |
68 |
68 |
69 |
69 |
70 /* download */ |
70 /* download */ |
71 |
71 |
72 Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path => |
72 Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path => |