src/Pure/Admin/build_release.scala

         progress = progress)
 
     def bundle_info(platform: Platform.Family.Value): Bundle_Info =
       platform match {
         case Platform.Family.linux =>
-          Bundle_Info(platform, "Linux", dist_name + "_app.tar.gz", None)
+          Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz", None)
         case Platform.Family.macos =>
-          Bundle_Info(platform, "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz"))
+          Bundle_Info(platform, "Mac OS X", dist_name + ".dmg", Some(dist_name + "_macos.tar.gz"))
         case Platform.Family.windows =>
           Bundle_Info(platform, "Windows", dist_name + ".exe", None)
       }
   }
 

         progress.echo_warning("Application bundle already exists: " + bundle_archive)
       else {
         val isabelle_name = release.dist_name
         val platform = bundle_info.platform
 
-        progress.echo("\nApplication bundle for " + platform + ": " + bundle_archive)
+        progress.echo("\nApplication bundle for " + platform)
 
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
         {
           // release archive
 

           }
 
           val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
 
 
-          // platform-specific setup (inside archive)
+          // application bundling
 
           platform match {
             case Platform.Family.linux =>
               File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
                 terminate_lines(java_options_title :: java_options))

               val linux_app = isabelle_target + Path.explode("contrib/linux_app")
               File.move(linux_app + Path.explode("Isabelle"),
                 isabelle_target + Path.explode(isabelle_name))
               Isabelle_System.rm_tree(linux_app)
 
+              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)) + " " +
+                Bash.string(isabelle_name))
+
             case Platform.Family.macos =>
-              File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
               File.write(isabelle_target + jedit_props,
                 File.read(isabelle_target + jedit_props)
                   .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
                   .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
                   .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
                   .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
 
+
+              // MacOS application bundle
+
+              File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
+              val dmg_dir = tmp_dir + Path.explode("macos_app/dmg")
+
+              val isabelle_app = Path.explode(isabelle_name + ".app")
+              val app_dir = dmg_dir + isabelle_app
+              File.move(dmg_dir + Path.explode("Isabelle.app"), app_dir)
+
+              val app_contents = app_dir + Path.explode("Contents")
+              val app_resources = app_contents + Path.explode("Resources")
+              File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
+
+              File.write(app_contents + Path.explode("Info.plist"),
+                File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
+                  .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+                  .replaceAllLiterally("{JAVA_OPTIONS}",
+                    terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
+
+              for (cp <- classpath) {
+                File.link(
+                  Path.explode("../Resources/" + isabelle_name + "/") + cp,
+                  app_contents + Path.explode("Java"),
+                  force = true)
+              }
+
+              File.link(
+                Path.explode("../Resources/" + isabelle_name + "/contrib/" +
+                  jdk_component + "/x86_64-darwin"),
+                app_contents + Path.explode("PlugIns/bundled.jdk"),
+                force = true)
+
+              File.link(
+                Path.explode("../../Info.plist"),
+                app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
+                force = true)
+
+              File.link(
+                Path.explode("Contents/Resources/" + isabelle_name),
+                app_dir + Path.explode("Isabelle"),
+                force = true)
+
+
+              // application archive: dmg or .tar.gz
+
+              val isabelle_dmg = Path.explode(isabelle_name + ".dmg")
+              (release.dist_dir + isabelle_dmg).file.delete
+
+              remote_mac match {
+                case SSH.Target(user, host) =>
+                  progress.echo("Packaging " + isabelle_dmg + " (via host " + quote(host) + ") ...")
+                  using(SSH.open_session(options, host = host, user = user))(ssh =>
+                  {
+                    val dmg_archive = Path.explode("dmg.tar")
+                    execute_tar(dmg_dir, "-cf " + File.bash_path(tmp_dir + dmg_archive) + " .")
+
+                    ssh.with_tmp_dir(remote_dir =>
+                    {
+                      val cd = "cd " + ssh.bash_path(remote_dir) + "; "
+                      ssh.write_file(remote_dir + dmg_archive, tmp_dir + dmg_archive)
+                      ssh.execute(
+                        cd + "mkdir dmg && tar -C dmg -xf " + ssh.bash_path(dmg_archive)).check
+                      ssh.execute(
+                        cd + "hdiutil create -srcfolder dmg -volname Isabelle " +
+                        ssh.bash_path(isabelle_dmg)).check
+                      ssh.read_file(remote_dir + isabelle_dmg, release.dist_dir + isabelle_dmg)
+                    })
+                  })
+                case _ =>
+                  val archive_name = isabelle_name + "_macos.tar.gz"
+                  progress.echo("Packaging " + archive_name + " ...")
+                  execute_tar(dmg_dir,
+                    "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+                    File.bash_path(isabelle_app))
+              }
+
             case Platform.Family.windows =>
-              val app_template = Path.explode("~~/Admin/Windows/launch4j")
-              val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
-
-              File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
-
               File.write(isabelle_target + jedit_props,
                 File.read(isabelle_target + jedit_props)
                   .replaceAll("lookAndFeel=.*",
                     "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
                   .replaceAll("foldPainter=.*", "foldPainter=Square"))
+
+
+              // application launcher
+
+              File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
+
+              val app_template = Path.explode("~~/Admin/Windows/launch4j")
 
               File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
                 (java_options_title :: java_options).map(_ + "\r\n").mkString)
 
               val isabelle_xml = Path.explode("isabelle.xml")

 
               File.copy(app_template + Path.explode("manifest.xml"),
                 isabelle_target + isabelle_exe.ext("manifest"))
 
 
+              // Cygwin setup
+
+              val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
+
               File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
 
               val cygwin_mirror =
                 File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
 

                 """> contrib/cygwin/isabelle/symlinks""")
 
               execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
 
               File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
-          }
-
-
-          // archive
-
-          val archive_name = isabelle_name + "_" + platform + ".tar.gz"
-          progress.echo("Packaging " + archive_name + " ...")
-          execute_tar(tmp_dir,
-            "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
-            Bash.string(isabelle_name))
-
-
-          // platform-specific application (outside archive)
-
-          progress.echo("Application for " + platform + " ...")
-
-          platform match {
-            case Platform.Family.linux =>
-              File.link(
-                Path.explode(isabelle_name + "_linux.tar.gz"),
-                release.dist_dir + Path.explode(isabelle_name + "_app.tar.gz"),
-                force = true)
-
-            case Platform.Family.macos =>
-              val dmg_dir = tmp_dir + Path.explode("macos_app/dmg")
-              val app_dir = dmg_dir + Path.explode(isabelle_name + ".app")
-              File.move(dmg_dir + Path.explode("Isabelle.app"), app_dir)
-
-              val app_contents = app_dir + Path.explode("Contents")
-              val app_resources = app_contents + Path.explode("Resources")
-              File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
-
-              File.write(app_contents + Path.explode("Info.plist"),
-                File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
-                  .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
-                  .replaceAllLiterally("{JAVA_OPTIONS}",
-                    terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
-
-              for (cp <- classpath) {
-                File.link(
-                  Path.explode("../Resources/" + isabelle_name + "/") + cp,
-                  app_contents + Path.explode("Java"),
-                  force = true)
-              }
-
-              File.link(
-                Path.explode("../Resources/" + isabelle_name + "/contrib/" +
-                  jdk_component + "/x86_64-darwin"),
-                app_contents + Path.explode("PlugIns/bundled.jdk"),
-                force = true)
-
-              File.link(
-                Path.explode("../../Info.plist"),
-                app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
-                force = true)
-
-              File.link(
-                Path.explode("Contents/Resources/" + isabelle_name),
-                app_dir + Path.explode("Isabelle"),
-                force = true)
-
-              val dmg = Path.explode(isabelle_name + ".dmg")
-              (release.dist_dir + dmg).file.delete
-
-              val dmg_archive = Path.explode(isabelle_name + "_dmg.tar.gz")
-              execute_tar(dmg_dir, "-czf " + File.bash_path(release.dist_dir + dmg_archive) + " .")
-
-              remote_mac match {
-                case SSH.Target(user, host) =>
-                  progress.echo("Building dmg on " + quote(host) + " ...")
-                  using(SSH.open_session(options, host = host, user = user))(ssh =>
-                  {
-                    ssh.with_tmp_dir(remote_dir =>
-                    {
-                      val cd = "cd " + ssh.bash_path(remote_dir) + "; "
-                      ssh.write_file(remote_dir + dmg_archive, release.dist_dir + dmg_archive)
-                      ssh.execute(
-                        cd + "mkdir root && tar -C root -xzf " + ssh.bash_path(dmg_archive)).check
-                      ssh.execute(
-                        cd + "hdiutil create -srcfolder root -volname Isabelle " +
-                        ssh.bash_path(dmg)).check
-                      ssh.read_file(remote_dir + dmg, release.dist_dir + dmg)
-                    })
-                  })
-                case _ =>
-              }
-
-            case Platform.Family.windows =>
+
+
+              // executable archive (self-extracting 7z)
+
               val exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z")
               exe_archive.file.delete
 
               execute(tmp_dir,
                 "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
               if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
 
-              val isabelle_exe = Path.explode(isabelle_name + ".exe")
               val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
               val sfx_txt =
                 File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
                   replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)