diff -r df7d7477284b -r 0698ded5caf1 src/Pure/System/components.scala --- a/src/Pure/System/components.scala Mon Dec 03 21:32:08 2018 +0100 +++ b/src/Pure/System/components.scala Mon Dec 03 22:07:23 2018 +0100 @@ -16,6 +16,20 @@ def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) + def download(dir: Path, names: List[String], progress: Progress = No_Progress) + { + Isabelle_System.mkdirs(dir) + for (name <- names) { + val archive = name + ".tar.gz" + val target = dir + Path.explode(archive) + if (!target.is_file) { + val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive + progress.echo("Getting " + quote(remote)) + Bytes.write(target, Url.read_bytes(Url(remote))) + } + } + } + /* component directory content */