# HG changeset patch
# User wenzelm
# Date 1506790418 -7200
# Node ID e76850a09a12966cf288149851bd5ab45f586c08
# Parent  1da2ef1fd8c1494782ae085089fdbc112b53e27d
tuned;

diff -r 1da2ef1fd8c1 -r e76850a09a12 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sat Sep 30 13:14:01 2017 +0200
+++ b/src/Pure/Admin/build_release.scala	Sat Sep 30 18:53:38 2017 +0200
@@ -12,15 +12,19 @@
   sealed case class Bundle_Info(
     platform_family: String,
     platform_description: String,
-    main_bundle: String,
-    fallback_bundle: Option[String])
+    main: String,
+    fallback: Option[String])
   {
-    def all_bundles: List[String] = main_bundle :: fallback_bundle.toList
+    def names: List[String] = main :: fallback.toList
   }
 
   sealed case class Release_Info(
-    date: Date, name: String, dist_dir: Path, dist_archive: Path, dist_library_archive: Path,
-      id: String)
+    date: Date,
+    name: String,
+    dist_dir: Path,
+    dist_archive: Path,
+    dist_library_archive: Path,
+    id: String)
   {
     val bundle_infos: List[Bundle_Info] =
       List(Bundle_Info("linux", "Linux", name + "_app.tar.gz", None),
@@ -28,7 +32,7 @@
         Bundle_Info("macos", "Mac OS X", name + ".dmg", Some(name + "_dmg.tar.gz")))
 
     def bundle_info(platform_family: String): Bundle_Info =
-      bundle_infos.find(info => info.platform_family == platform_family) getOrElse
+      bundle_infos.find(bundle_info => bundle_info.platform_family == platform_family) getOrElse
         error("Unknown platform family " + quote(platform_family))
   }
 
@@ -94,18 +98,18 @@
 
     /* make application bundles */
 
-    for (info <- bundle_infos) {
+    for (bundle_info <- bundle_infos) {
       val bundle =
-        (if (remote_mac.isEmpty) info.fallback_bundle else None) getOrElse info.main_bundle
+        (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main
       val bundle_archive = release_info.dist_dir + Path.explode(bundle)
       if (bundle_archive.is_file)
         progress.echo("### Application bundle already exists: " + bundle_archive.implode)
       else {
         progress.echo(
-          "\nApplication bundle for " + info.platform_family + ": " + bundle_archive.implode)
+          "\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive.implode)
         progress.bash(
           "isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) +
-            " " + Bash.string(info.platform_family) +
+            " " + Bash.string(bundle_info.platform_family) +
             (if (remote_mac == "") "" else " " + Bash.string(remote_mac)),
           echo = true).check
       }
@@ -117,10 +121,10 @@
     for (dir <- website) {
       val website_platform_bundles =
         for {
-          info <- bundle_infos
+          bundle_info <- bundle_infos
           bundle <-
-            info.all_bundles.find(name => (release_info.dist_dir + Path.explode(name)).is_file)
-        } yield (bundle, info)
+            bundle_info.names.find(name => (release_info.dist_dir + Path.explode(name)).is_file)
+        } yield (bundle, bundle_info)
 
       val afp_link =
         HTML.link("https://bitbucket.org/isa-afp/afp-devel/commits/" + afp_rev,
@@ -131,8 +135,8 @@
         List(
           HTML.chapter(release_info.name + " (" + release_id + ")"),
           HTML.itemize(
-            website_platform_bundles.map({ case (bundle, info) =>
-              List(HTML.link(bundle, HTML.text(info.platform_description))) }))) :::
+            website_platform_bundles.map({ case (bundle, bundle_info) =>
+              List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) :::
         (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link)))))
 
       for ((bundle, _) <- website_platform_bundles)