# HG changeset patch
# User wenzelm
# Date 1619704144 -7200
# Node ID 6ba5f9d18c56de0831b542962dd93deaee9368cf
# Parent  58b17dca57ef40e9defb292c7820a4743029cac5
clarified signature: more operations;

diff -r 58b17dca57ef -r 6ba5f9d18c56 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Apr 28 23:20:05 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Thu Apr 29 15:49:04 2021 +0200
@@ -759,10 +759,11 @@
         } yield (bundle_info.name, bundle_info)
 
       val isabelle_link =
-        HTML.link(Isabelle_System.isabelle_repository.rev(release.ident),
+        HTML.link(Isabelle_System.isabelle_repository.changeset(release.ident),
           HTML.text("Isabelle/" + release.ident))
       val afp_link =
-        HTML.link(Isabelle_System.afp_repository.rev(afp_rev), HTML.text("AFP/" + afp_rev))
+        HTML.link(Isabelle_System.afp_repository.changeset(afp_rev),
+          HTML.text("AFP/" + afp_rev))
 
       HTML.write_document(dir, "index.html",
         List(HTML.title(release.dist_name)),
diff -r 58b17dca57ef -r 6ba5f9d18c56 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Wed Apr 28 23:20:05 2021 +0200
+++ b/src/Pure/General/mercurial.scala	Thu Apr 29 15:49:04 2021 +0200
@@ -28,7 +28,36 @@
   {
     override def toString: String = root
 
-    def rev(r: String): String = root + "/rev/" + r
+    def changeset(rev: String = "tip", raw: Boolean = false): String =
+      root + (if (raw) "/raw-rev/" else "/rev/") + rev
+
+    def file(path: Path, rev: String = "tip", raw: Boolean = false): String =
+      root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + path.expand.implode
+
+    def archive(rev: String = "tip"): String =
+      root + "/archive/" + rev + ".tar.gz"
+
+    def read_changeset(rev: String = "tip"): String =
+      Url.read(changeset(rev = rev, raw = true))
+
+    def read_file(path: Path, rev: String = "tip"): String =
+      Url.read(file(path, rev = rev, raw = true))
+
+    def download_archive(rev: String = "tip", progress: Progress = new Progress): HTTP.Content =
+      Isabelle_System.download(archive(rev = rev), progress = progress)
+
+    def download_dir(dir: Path, rev: String = "tip", progress: Progress = new Progress): Unit =
+    {
+      Isabelle_System.new_directory(dir)
+      Isabelle_System.with_tmp_file("rev", ext = ".tar.gz")(archive_path =>
+      {
+        val content = download_archive(rev = rev, progress = progress)
+        Bytes.write(archive_path, content.bytes)
+        progress.echo("Unpacking " + rev + ".tar.gz")
+        Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path) + " --strip-components=1",
+          dir = dir, original_owner = true).check
+      })
+    }
   }
 
 
diff -r 58b17dca57ef -r 6ba5f9d18c56 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Apr 28 23:20:05 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Apr 29 15:49:04 2021 +0200
@@ -626,4 +626,8 @@
 
   val afp_repository: Mercurial.Address =
     Mercurial.Address("https://isabelle.sketis.net/repos/afp-devel")
+
+  def official_releases(): List[String] =
+    Library.trim_split_lines(
+      isabelle_repository.read_file(Path.explode("Admin/Release/official")))
 }