# HG changeset patch
# User wenzelm
# Date 1544102727 -3600
# Node ID c071fcec43232a9ee44e2f5207d1df2c16e1575b
# Parent  e7a5340128f008419890119eca281849030dff92
more explicit Platform.Family;

diff -r e7a5340128f0 -r c071fcec4323 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Thu Dec 06 12:55:53 2018 +0100
+++ b/src/Pure/Admin/build_release.scala	Thu Dec 06 14:25:27 2018 +0100
@@ -12,7 +12,7 @@
   /** release info **/
 
   sealed case class Bundle_Info(
-    platform_family: String,
+    platform: Platform.Family.Value,
     platform_description: String,
     main: String,
     fallback: Option[String])
@@ -37,13 +37,14 @@
         isabelle_identifier = dist_name + "-build",
         progress = progress)
 
-    def bundle_info(platform_family: String): Bundle_Info =
-      platform_family match {
-        case "linux" => Bundle_Info("linux", "Linux", dist_name + "_app.tar.gz", None)
-        case "windows" => Bundle_Info("windows", "Windows", dist_name + ".exe", None)
-        case "macos" =>
-          Bundle_Info("macos", "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz"))
-        case _ => error("Unknown platform family " + quote(platform_family))
+    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)
+        case Platform.Family.macos =>
+          Bundle_Info(platform, "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz"))
+        case Platform.Family.windows =>
+          Bundle_Info(platform, "Windows", dist_name + ".exe", None)
       }
   }
 
@@ -135,13 +136,13 @@
 
   /* bundled components */
 
-  class Bundled(platform: String = "")
+  class Bundled(platform: Option[Platform.Family.Value] = None)
   {
     def detect(s: String): Boolean =
       s.startsWith("#bundled") && !s.startsWith("#bundled ")
 
     def apply(name: String): String =
-      "#bundled" + (if (platform == "") "" else "-" + platform) + ":" + name
+      "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
 
     private val Pattern1 = ("""^#bundled:(.*)$""").r
     private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
@@ -149,7 +150,7 @@
     def unapply(s: String): Option[String] =
       s match {
         case Pattern1(name) => Some(name)
-        case Pattern2(platform1, name) if platform == platform1 => Some(name)
+        case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
         case _ => None
       }
   }
@@ -159,7 +160,8 @@
     val catalogs =
       List("main", "bundled").map((_, new Bundled())) :::
       default_platform_families.flatMap(platform =>
-        List(platform, "bundled-" + platform).map((_, new Bundled(platform = platform))))
+        List(platform.toString, "bundled-" + platform.toString).
+          map((_, new Bundled(platform = Some(platform)))))
 
     File.append(Components.components(dir),
       terminate_lines("#bundled components" ::
@@ -172,9 +174,9 @@
         } yield bundled(line)).toList))
   }
 
-  def get_bundled_components(dir: Path, platform: String): (List[String], String) =
+  def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
   {
-    val Bundled = new Bundled(platform)
+    val Bundled = new Bundled(platform = Some(platform))
     val components =
       for {
         Bundled(name) <- Components.read_components(dir)
@@ -185,9 +187,9 @@
     (components, jdk_component)
   }
 
-  def activate_bundled_components(dir: Path, platform: String)
+  def activate_bundled_components(dir: Path, platform: Platform.Family.Value)
   {
-    val Bundled = new Bundled(platform)
+    val Bundled = new Bundled(platform = Some(platform))
     Components.write_components(dir,
       Components.read_components(dir).flatMap(line =>
         line match {
@@ -222,7 +224,8 @@
   private def tar_options: String =
     if (Platform.is_macos) "--owner=root --group=staff" else "--owner=root --group=root"
 
-  private val default_platform_families = List("linux", "windows", "macos")
+  private val default_platform_families =
+    List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
 
   def build_release(base_dir: Path,
     options: Options,
@@ -232,7 +235,7 @@
     afp_rev: String = "",
     official_release: Boolean = false,
     proper_release_name: Option[String] = None,
-    platform_families: List[String] = default_platform_families,
+    platform_families: List[Platform.Family.Value] = default_platform_families,
     website: Option[Path] = None,
     build_library: Boolean = false,
     parallel_jobs: Int = 1,
@@ -396,7 +399,7 @@
         progress.echo_warning("Application bundle already exists: " + bundle_archive)
       else {
         val isabelle_name = release.dist_name
-        val platform = bundle_info.platform_family
+        val platform = bundle_info.platform
 
         progress.echo("\nApplication bundle for " + platform + ": " + bundle_archive)
 
@@ -456,7 +459,7 @@
 
           // platform-specific setup (inside archive)
 
-          if (platform == "linux") {
+          if (platform == Platform.Family.linux) {
             File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
               terminate_lines(java_options_title :: java_options))
 
@@ -473,7 +476,7 @@
               isabelle_target + Path.explode(isabelle_name))
             Isabelle_System.rm_tree(linux_app)
           }
-          else if (platform == "macos") {
+          else if (platform == 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)
@@ -482,7 +485,7 @@
                 .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
                 .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
           }
-          else if (platform == "windows") {
+          else if (platform == Platform.Family.windows) {
             val app_template = Path.explode("~~/Admin/Windows/launch4j")
             val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
 
@@ -565,13 +568,13 @@
 
           progress.echo("Application for " + platform + " ...")
 
-          if (platform == "linux") {
+          if (platform == Platform.Family.linux) {
             File.link(
               Path.explode(isabelle_name + "_linux.tar.gz"),
               release.dist_dir + Path.explode(isabelle_name + "_app.tar.gz"),
               force = true)
           }
-          else if (platform == "macos") {
+          else if (platform == 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)
@@ -635,7 +638,7 @@
               case _ =>
             }
           }
-          else if (platform == "windows") {
+          else if (platform == Platform.Family.windows) {
             val exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z")
             exe_archive.file.delete
 
@@ -694,9 +697,8 @@
       else {
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
-            val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY")
             val bundle =
-              release.dist_dir + Path.explode(release.dist_name + "_" + platform + ".tar.gz")
+              release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
             execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
 
             val other_isabelle = release.other_isabelle(tmp_dir)
@@ -767,7 +769,7 @@
         "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
         "l" -> (_ => build_library = true),
         "o:" -> (arg => options = options + arg),
-        "p:" -> (arg => platform_families = space_explode(',', arg)),
+        "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
         "r:" -> (arg => rev = arg))
 
       val more_args = getopts(args)
diff -r e7a5340128f0 -r c071fcec4323 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Thu Dec 06 12:55:53 2018 +0100
+++ b/src/Pure/System/components.scala	Thu Dec 06 14:25:27 2018 +0100
@@ -39,16 +39,15 @@
     }
   }
 
-  def purge(dir: Path, platform: String)
+  def purge(dir: Path, platform: Platform.Family.Value)
   {
     def purge_platforms(platforms: String*): Set[String] =
       platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin"
     val purge_set =
       platform match {
-        case "linux" => purge_platforms("darwin", "cygwin", "windows")
-        case "windows" => purge_platforms("linux", "darwin")
-        case "macos" => purge_platforms("linux", "cygwin", "windows")
-        case _ => error("Bad platform: " + quote(platform))
+        case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows")
+        case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows")
+        case Platform.Family.windows => purge_platforms("linux", "darwin")
       }
 
     File.find_files(dir.file,
diff -r e7a5340128f0 -r c071fcec4323 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Thu Dec 06 12:55:53 2018 +0100
+++ b/src/Pure/System/platform.scala	Thu Dec 06 14:25:27 2018 +0100
@@ -15,6 +15,24 @@
   val is_macos = System.getProperty("os.name", "") == "Mac OS X"
   val is_windows = System.getProperty("os.name", "").startsWith("Windows")
 
+  def family: Family.Value =
+    if (is_linux) Family.linux
+    else if (is_macos) Family.macos
+    else if (is_windows) Family.windows
+    else error("Failed to determine current platform family")
+
+  object Family extends Enumeration
+  {
+    val linux, macos, windows = Value
+
+    def unapply(name: String): Option[Value] =
+      try { Some(withName(name)) }
+      catch { case _: NoSuchElementException => None }
+
+    def parse(name: String): Value =
+      unapply(name) getOrElse error("Bad platform family: " + quote(name))
+  }
+
 
   /* platform identifiers */