# HG changeset patch
# User wenzelm
# Date 1543871243 -3600
# Node ID 0698ded5caf14962594abb813435f247e82c6fca
# Parent  df7d7477284be1460a920edface295e9abc748d8
Components.download similar to "isabelle components", but without unpacking;

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 */