# HG changeset patch
# User wenzelm
# Date 1620151328 -7200
# Node ID f8f065e208377ab62a5cb687db2bb5cd3318bd19
# Parent  f033d4f661e94aec6991fc929f446d68166a0989
misc tuning and clarification: more explicit types Release_Context, Release_Archive;

diff -r f033d4f661e9 -r f8f065e20837 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Tue May 04 12:54:54 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Tue May 04 20:02:08 2021 +0200
@@ -9,7 +9,72 @@
 
 object Build_Release
 {
-  /** release info **/
+  /** release context **/
+
+  object Release_Context
+  {
+    def apply(
+      target_dir: Path,
+      release_name: String = "",
+      components_base: Path = Components.default_components_base,
+      progress: Progress = new Progress): Release_Context =
+    {
+      val date = Date.now()
+      val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
+      val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
+      new Release_Context(release_name, dist_name, dist_dir, components_base, progress)
+    }
+  }
+
+  class Release_Context private[Build_Release](
+    val release_name: String,
+    val dist_name: String,
+    val dist_dir: Path,
+    val components_base: Path,
+    val progress: Progress)
+  {
+    override def toString: String = dist_name
+
+    val isabelle: Path = Path.explode(dist_name)
+    val isabelle_dir: Path = dist_dir + isabelle
+    val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
+    val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
+
+    def other_isabelle(dir: Path): Other_Isabelle =
+      Other_Isabelle(dir + isabelle,
+        isabelle_identifier = dist_name + "-build",
+        progress = progress)
+
+    def make_announce(id: String): Unit =
+    {
+      if (release_name.isEmpty) {
+        File.write(isabelle_dir + Path.explode("ANNOUNCE"),
+          """
+IMPORTANT NOTE
+==============
+
+This is a snapshot of Isabelle/""" + id + """ from the repository.
+""")
+      }
+    }
+
+    def make_contrib(): Unit =
+    {
+      Isabelle_System.make_directory(Components.contrib(isabelle_dir))
+      File.write(Components.contrib(isabelle_dir, name = "README"),
+        """This directory contains add-on components that contribute to the main
+Isabelle distribution.  Separate licensing conditions apply, see each
+directory individually.
+""")
+    }
+
+    def bundle_info(platform: Platform.Family.Value): Bundle_Info =
+      platform match {
+        case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
+        case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
+        case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
+      }
+  }
 
   sealed case class Bundle_Info(
     platform: Platform.Family.Value,
@@ -19,72 +84,46 @@
     def path: Path = Path.explode(name)
   }
 
-  class Release private[Build_Release](
-    progress: Progress,
-    val date: Date,
-    val dist_name: String,
-    val dist_dir: Path,
-    val dist_version: String,
-    val ident: String,
-    val tags: String)
+
+
+  /** release archive **/
+
+  val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID")
+  val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS")
+  val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER")
+
+  object Release_Archive
   {
-    val isabelle: Path = Path.explode(dist_name)
-    val isabelle_dir: Path = dist_dir + isabelle
-    val isabelle_id: Path = isabelle_dir + Path.explode("etc/ISABELLE_ID")
-    val isabelle_tags: Path = isabelle_dir + Path.explode("etc/ISABELLE_TAGS")
-    val isabelle_identifier: Path = isabelle_dir + Path.explode("etc/ISABELLE_IDENTIFIER")
-    val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
-    val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
+    def make(bytes: Bytes): Release_Archive =
+    {
+      Isabelle_System.with_tmp_dir("tmp")(dir =>
+        Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
+        {
+          Bytes.write(archive_path, bytes)
+          Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
+            dir = dir, original_owner = true, strip = 1).check
 
-    def other_isabelle(dir: Path): Other_Isabelle =
-      Other_Isabelle(dir + isabelle,
-        isabelle_identifier = dist_name + "-build",
-        progress = progress)
+          val id = File.read(dir + ISABELLE_ID)
+          val tags = File.read(dir + ISABELLE_TAGS)
+          val identifier = File.read(dir + ISABELLE_IDENTIFIER)
+          new Release_Archive(bytes, id, tags, identifier)
+        })
+      )
+    }
 
-    def bundle_info(platform: Platform.Family.Value): Bundle_Info =
-      platform match {
-        case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
-        case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
-        case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
-      }
+    def read(path: Path): Release_Archive = make(Bytes.read(path))
+  }
+
+  case class Release_Archive private[Build_Release](
+    bytes: Bytes, id: String, tags: String, identifier: String)
+  {
+    override def toString: String = identifier
   }
 
 
 
   /** generated content **/
 
-  /* ANNOUNCE */
-
-  def make_announce(release: Release): Unit =
-  {
-    File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
-"""
-IMPORTANT NOTE
-==============
-
-This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
-
-""")
-  }
-
-
-  /* NEWS */
-
-  def make_news(other_isabelle: Other_Isabelle, dist_version: String): Unit =
-  {
-    val target = other_isabelle.isabelle_home + Path.explode("doc")
-    val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts"))
-    other_isabelle.copy_fonts(target_fonts)
-
-    HTML.write_document(target, "NEWS.html",
-      List(HTML.title("NEWS (" + dist_version + ")")),
-      List(
-        HTML.chapter("NEWS"),
-        HTML.source(
-          Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
-  }
-
-
   /* bundled components */
 
   class Bundled(platform: Option[Platform.Family.Value] = None)
@@ -155,17 +194,6 @@
         }) ::: more_names.map(contrib_name))
   }
 
-  def make_contrib(dir: Path): Unit =
-  {
-    Isabelle_System.make_directory(Components.contrib(dir))
-    File.write(Components.contrib(dir, "README"),
-"""This directory contains add-on components that contribute to the main
-Isabelle distribution.  Separate licensing conditions apply, see each
-directory individually.
-""")
-  }
-
-
 
   /** build release **/
 
@@ -188,8 +216,7 @@
     options.string(server_option) match {
       case SSH.Target(user, host) =>
         using(SSH.open_session(options, host = host, user = user))(ssh =>
-        {
-          Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar =>
+          Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
           {
             execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
             ssh.with_tmp_dir(remote_dir =>
@@ -200,14 +227,14 @@
                 List(
                   "cd " + File.bash_path(remote_dir),
                   "tar -xf tmp.tar",
-                  "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
+                  "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
                   "tar -cf tmp.tar heaps")
               ssh.execute(remote_commands.mkString(" && ")).check
               ssh.read_file(remote_tmp_tar, local_tmp_tar)
             })
             execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
           })
-        })
+        )
       case s => error("Bad " + server_option + ": " + quote(s))
     }
   }
@@ -340,119 +367,73 @@
   private val default_platform_families: List[Platform.Family.Value] =
     List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
 
-  def build_release(options: Options,
-    target_dir: Path = Path.current,
-    components_base: Path = Components.default_components_base,
-    progress: Progress = new Progress,
-    rev: String = "",
-    afp_rev: String = "",
-    proper_release_name: Option[String] = None,
-    platform_families: List[Platform.Family.Value] = default_platform_families,
-    more_components: List[Path] = Nil,
-    website: Option[Path] = None,
-    build_sessions: List[String] = Nil,
-    build_library: Boolean = false,
-    parallel_jobs: Int = 1): Release =
+  def build_release_archive(
+    context: Release_Context,
+    version: String,
+    parallel_jobs: Int = 1): Release_Archive =
   {
-    val hg = Mercurial.repository(Path.ISABELLE_HOME)
-
-    val release =
-    {
-      val date = Date.now()
-      val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
-      val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
-
-      val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
-      val ident =
-        try { hg.id(version) }
-        catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
-      val tags = hg.tags(rev = ident)
+    val progress = context.progress
 
-      val dist_version =
-        proper_release_name match {
-          case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
-          case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
-        }
-
-      new Release(progress, date, dist_name, dist_dir, dist_version, ident, tags)
-    }
-
-
-    /* make distribution */
+    val hg = Mercurial.repository(Path.ISABELLE_HOME)
+    val id =
+      try { hg.id(version) }
+      catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
 
-    if (release.isabelle_archive.is_file) {
-      progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
+    if (context.isabelle_archive.is_file) {
+      progress.echo_warning("Found existing release archive: " + context.isabelle_archive)
 
-      val archive_ident =
-        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
-          {
-            val isabelle_id = release.isabelle + Path.explode("etc/ISABELLE_ID")
-            execute_tar(tmp_dir, "-xzf " +
-              File.bash_path(release.isabelle_archive) + " " + File.bash_path(isabelle_id))
-            Isabelle_System.isabelle_id(root = tmp_dir + release.isabelle)
-          })
-
-      if (release.ident != archive_ident) {
-        error("Mismatch of release identification " + release.ident +
-          " vs. archive " + archive_ident)
-      }
+      val archive = Release_Archive.read(context.isabelle_archive)
+      if (id == archive.id) archive
+      else error("Mismatch of release identification " + id + " vs. archive " + archive.id)
     }
     else {
-      progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
-
-      Isabelle_System.make_directory(release.dist_dir)
+      progress.echo_warning("Preparing release " + context.dist_name + " ...")
 
-      if (release.isabelle_dir.is_dir)
-        error("Directory " + release.isabelle_dir + " already exists")
-
+      Isabelle_System.new_directory(context.dist_dir)
 
-      progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
-
-      hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
+      hg.archive(context.isabelle_dir.expand.implode, rev = id, options = "--type files")
 
       for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
-        (release.isabelle_dir + Path.explode(name)).file.delete
+        (context.isabelle_dir + Path.explode(name)).file.delete
       }
 
-
-      progress.echo_warning("Preparing distribution " + quote(release.dist_name))
+      File.write(context.isabelle_dir + ISABELLE_ID, id)
+      File.write(context.isabelle_dir + ISABELLE_TAGS, hg.tags(rev = id))
+      File.write(context.isabelle_dir + ISABELLE_IDENTIFIER, context.dist_name)
 
-      File.write(release.isabelle_id, release.ident)
-      File.write(release.isabelle_tags, release.tags)
-      File.write(release.isabelle_identifier, release.dist_name)
+      context.make_announce(id)
 
-      if (proper_release_name.isEmpty) make_announce(release)
-
-      make_contrib(release.isabelle_dir)
+      context.make_contrib()
 
-      execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
+      execute(context.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
 
-      record_bundled_components(release.isabelle_dir)
+      record_bundled_components(context.isabelle_dir)
 
 
       /* build tools and documentation */
 
-      val other_isabelle = release.other_isabelle(release.dist_dir)
+      val other_isabelle = context.other_isabelle(context.dist_dir)
 
       other_isabelle.init_settings(
-        other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
+        other_isabelle.init_components(
+          components_base = context.components_base, catalogs = List("main")))
       other_isabelle.resolve_components(echo = true)
 
       try {
         val export_classpath =
           "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
-        other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
-        other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
+        other_isabelle.bash(export_classpath + "Admin/build all", echo = true).check
+        other_isabelle.bash(export_classpath + "bin/isabelle jedit -b", echo = true).check
       }
       catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
 
       try {
         other_isabelle.bash(
-          "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
+          "bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
       }
       catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
 
-      make_news(other_isabelle, release.dist_version)
+      other_isabelle.make_news()
 
       for (name <- List("Admin", "browser_info", "heaps")) {
         Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
@@ -461,52 +442,59 @@
       other_isabelle.cleanup()
 
 
-      progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
-
-      def execute_dist_name(script: String): Unit =
-        Isabelle_System.bash(script, cwd = release.dist_dir.file,
-          env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
-
-      execute_dist_name("""
-set -e
+      progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...")
 
-chmod -R a+r "$DIST_NAME"
-chmod -R u+w "$DIST_NAME"
-chmod -R g=o "$DIST_NAME"
-find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
-""")
+      execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""")
+      execute(context.dist_dir,
+        """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
+      execute_tar(context.dist_dir, "-czf " +
+        File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
 
-      execute_tar(release.dist_dir, "-czf " +
-        File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
+      Release_Archive.read(context.isabelle_archive)
+    }
+  }
 
-      execute_dist_name("""
-set -e
+  def build_release(
+    options: Options,
+    context: Release_Context,
+    release_archive: Release_Archive,
+    afp_rev: String = "",
+    platform_families: List[Platform.Family.Value] = default_platform_families,
+    more_components: List[Path] = Nil,
+    website: Option[Path] = None,
+    build_sessions: List[String] = Nil,
+    build_library: Boolean = false,
+    parallel_jobs: Int = 1): Unit =
+  {
+    val progress = context.progress
 
-mv "$DIST_NAME" "${DIST_NAME}-old"
-mkdir "$DIST_NAME"
+
+    /* release directory */
 
-mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
-  "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
-mkdir "$DIST_NAME/doc"
-mv "${DIST_NAME}-old/doc/"*.pdf \
-  "${DIST_NAME}-old/doc/"*.html \
-  "${DIST_NAME}-old/doc/"*.css \
-  "${DIST_NAME}-old/doc/fonts" \
-  "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
+    for (name <- List(context.dist_name, "Isabelle")) {
+      Isabelle_System.rm_tree(context.dist_dir + Path.explode(name))
+    }
 
-rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
+    Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
+    {
+      Bytes.write(archive_path, release_archive.bytes)
+      val extract =
+        List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
+          map(name => context.dist_name + "/" + name)
+      execute_tar(context.dist_dir,
+        "-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
+    })
 
-rm -rf "${DIST_NAME}-old"
-""")
-    }
+    Isabelle_System.symlink(
+      Path.explode(context.dist_name), context.dist_dir + Path.explode("Isabelle"))
 
 
     /* make application bundles */
 
-    val bundle_infos = platform_families.map(release.bundle_info)
+    val bundle_infos = platform_families.map(context.bundle_info)
 
     for (bundle_info <- bundle_infos) {
-      val isabelle_name = release.dist_name
+      val isabelle_name = context.dist_name
       val platform = bundle_info.platform
 
       progress.echo("\nApplication bundle for " + platform)
@@ -515,8 +503,8 @@
       {
         // release archive
 
-        execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
-        val other_isabelle = release.other_isabelle(tmp_dir)
+        execute_tar(tmp_dir, "-xzf " + File.bash_path(context.isabelle_archive))
+        val other_isabelle = context.other_isabelle(tmp_dir)
         val isabelle_target = other_isabelle.isabelle_home
 
 
@@ -529,9 +517,9 @@
         val (bundled_components, jdk_component) =
           get_bundled_components(isabelle_target, platform)
 
-        Components.resolve(components_base, bundled_components,
+        Components.resolve(context.components_base, bundled_components,
           target_dir = Some(contrib_dir),
-          copy_dir = Some(release.dist_dir + Path.explode("contrib")),
+          copy_dir = Some(context.dist_dir + Path.explode("contrib")),
           progress = progress)
 
         val more_components_names =
@@ -606,7 +594,7 @@
             val archive_name = isabelle_name + "_linux.tar.gz"
             progress.echo("Packaging " + archive_name + " ...")
             execute_tar(tmp_dir,
-              "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+              "-czf " + File.bash_path(context.dist_dir + Path.explode(archive_name)) + " " +
               Bash.string(isabelle_name))
 
 
@@ -626,7 +614,7 @@
             }
 
             make_isabelle_plist(
-              app_contents + Path.explode("Info.plist"), isabelle_name, release.ident)
+              app_contents + Path.explode("Info.plist"), isabelle_name, release_archive.id)
 
             make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
               classpath, dock_icon = true)
@@ -647,7 +635,7 @@
               tmp_dir + isabelle_app)
 
             execute_tar(tmp_dir,
-              "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+              "-czf " + File.bash_path(context.dist_dir + Path.explode(archive_name)) + " " +
               File.bash_path(isabelle_app))
 
 
@@ -740,9 +728,9 @@
               File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt"))
                 .replace("{ISABELLE_NAME}", isabelle_name)
 
-            Bytes.write(release.dist_dir + isabelle_exe,
+            Bytes.write(context.dist_dir + isabelle_exe,
               Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
-            File.set_executable(release.dist_dir + isabelle_exe, true)
+            File.set_executable(context.dist_dir + isabelle_exe, true)
         }
       })
       progress.echo("DONE")
@@ -755,20 +743,20 @@
       val website_platform_bundles =
         for {
           bundle_info <- bundle_infos
-          if (release.dist_dir + bundle_info.path).is_file
+          if (context.dist_dir + bundle_info.path).is_file
         } yield (bundle_info.name, bundle_info)
 
       val isabelle_link =
-        HTML.link(Isabelle_System.isabelle_repository.changeset(release.ident),
-          HTML.text("Isabelle/" + release.ident))
+        HTML.link(Isabelle_System.isabelle_repository.changeset(release_archive.id),
+          HTML.text("Isabelle/" + release_archive.id))
       val afp_link =
         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)),
+        List(HTML.title(context.dist_name)),
         List(
-          HTML.section(release.dist_name),
+          HTML.section(context.dist_name),
           HTML.subsection("Platforms"),
           HTML.itemize(
             website_platform_bundles.map({ case (bundle, bundle_info) =>
@@ -778,24 +766,24 @@
             List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
 
       for ((bundle, _) <- website_platform_bundles)
-        Isabelle_System.copy_file(release.dist_dir + Path.explode(bundle), dir)
+        Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir)
     }
 
 
     /* HTML library */
 
     if (build_library) {
-      if (release.isabelle_library_archive.is_file) {
-        progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
+      if (context.isabelle_library_archive.is_file) {
+        progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
       }
       else {
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
             val bundle =
-              release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
+              context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
             execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
 
-            val other_isabelle = release.other_isabelle(tmp_dir)
+            val other_isabelle = context.other_isabelle(tmp_dir)
 
             Isabelle_System.make_directory(other_isabelle.etc)
             File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
@@ -805,15 +793,13 @@
               " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
             other_isabelle.isabelle_home_user.file.delete
 
-            execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
-            execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
-            execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
-              " " + Bash.string(release.dist_name + "/browser_info"))
+            execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name))
+            execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
+            execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
+              " " + Bash.string(context.dist_name + "/browser_info"))
           })
       }
     }
-
-    release
   }
 
 
@@ -826,7 +812,7 @@
       var afp_rev = ""
       var components_base: Path = Components.default_components_base
       var target_dir = Path.current
-      var proper_release_name: Option[String] = None
+      var release_name = ""
       var website: Option[Path] = None
       var build_sessions: List[String] = Nil
       var more_components: List[Path] = Nil
@@ -844,7 +830,7 @@
     -C DIR       base directory for Isabelle components (default: """ +
         Components.default_components_base + """)
     -D DIR       target directory (default ".")
-    -R RELEASE   proper release with name
+    -R RELEASE   explicit release name
     -W WEBSITE   produce minimal website in given directory
     -b SESSIONS  build platform-specific session images (separated by commas)
     -c ARCHIVE   clean bundling with additional component .tar.gz archive
@@ -859,7 +845,7 @@
         "A:" -> (arg => afp_rev = arg),
         "C:" -> (arg => components_base = Path.explode(arg)),
         "D:" -> (arg => target_dir = Path.explode(arg)),
-        "R:" -> (arg => proper_release_name = Some(arg)),
+        "R:" -> (arg => release_name = arg),
         "W:" -> (arg => website = Some(Path.explode(arg))),
         "b:" -> (arg => build_sessions = space_explode(',', arg)),
         "c:" -> (arg =>
@@ -877,19 +863,24 @@
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
-      val progress = new Console_Progress()
+      val context =
+        Release_Context(target_dir,
+          release_name = release_name,
+          components_base = components_base,
+          progress = new Console_Progress())
 
       if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
         error("Building for windows requires 7z")
 
-      build_release(options, target_dir = target_dir, components_base = components_base,
-        progress = progress, rev = rev, afp_rev = afp_rev,
-        proper_release_name = proper_release_name, website = website,
+      val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
+      val release_archive = build_release_archive(context, version, parallel_jobs = parallel_jobs)
+
+      build_release(options, context, release_archive, afp_rev = afp_rev,
         platform_families =
           if (platform_families.isEmpty) default_platform_families
           else platform_families,
         more_components = more_components, build_sessions = build_sessions,
-        build_library = build_library, parallel_jobs = parallel_jobs)
+        build_library = build_library, parallel_jobs = parallel_jobs, website = website)
     }
   }
 }
diff -r f033d4f661e9 -r f8f065e20837 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue May 04 12:54:54 2021 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue May 04 20:02:08 2021 +0200
@@ -85,7 +85,7 @@
   val build_release: Logger_Task =
     Logger_Task("build_release", logger =>
       {
-        Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev())
+        Isabelle_Devel.release_snapshot(logger.options, get_rev(), get_afp_rev())
       })
 
 
diff -r f033d4f661e9 -r f8f065e20837 src/Pure/Admin/isabelle_devel.scala
--- a/src/Pure/Admin/isabelle_devel.scala	Tue May 04 12:54:54 2021 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala	Tue May 04 20:02:08 2021 +0200
@@ -34,22 +34,19 @@
 
   /* release snapshot */
 
-  def release_snapshot(
-    options: Options,
-    rev: String = "",
-    afp_rev: String = "",
-    parallel_jobs: Int = 1): Unit =
+  def release_snapshot(options: Options, rev: String, afp_rev: String): Unit =
   {
     Isabelle_System.with_tmp_dir("isadist")(target_dir =>
       {
         Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
           website_dir =>
-            Build_Release.build_release(options, target_dir = target_dir,
-              rev = rev,
-              afp_rev = afp_rev,
-              parallel_jobs = parallel_jobs,
-              build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
-              website = Some(website_dir)))
+        {
+          val context = Build_Release.Release_Context(target_dir)
+          val release_archive = Build_Release.build_release_archive(context, rev)
+          Build_Release.build_release(options, context, release_archive, afp_rev = afp_rev,
+            build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
+            website = Some(website_dir))
+        })
       })
   }
 
diff -r f033d4f661e9 -r f8f065e20837 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Tue May 04 12:54:54 2021 +0200
+++ b/src/Pure/Admin/other_isabelle.scala	Tue May 04 20:02:08 2021 +0200
@@ -63,9 +63,23 @@
   val etc_settings: Path = etc + Path.explode("settings")
   val etc_preferences: Path = etc + Path.explode("preferences")
 
-  def copy_fonts(target_dir: Path): Unit =
+
+  /* NEWS */
+
+  def make_news(): Unit =
+  {
+    val doc_dir = isabelle_home + Path.explode("doc")
+    val fonts_dir = Isabelle_System.make_directory(doc_dir + Path.explode("fonts"))
+
     Isabelle_Fonts.make_entries(getenv = getenv, hidden = true).
-      foreach(entry => Isabelle_System.copy_file(entry.path, target_dir))
+      foreach(entry => Isabelle_System.copy_file(entry.path, fonts_dir))
+
+    HTML.write_document(doc_dir, "NEWS.html",
+      List(HTML.title("NEWS")),
+      List(
+        HTML.chapter("NEWS"),
+        HTML.source(Symbol.decode(File.read(isabelle_home + Path.explode("NEWS"))))))
+  }
 
 
   /* components */