# HG changeset patch
# User wenzelm
# Date 1693322974 -7200
# Node ID fd1fec53665b63b9b6ad78e4728f04dcf8565ff9
# Parent  67492b2a3a626b16d133a7c228998fe8e2ca7084
clarified signature: prefer enum types;

diff -r 67492b2a3a62 -r fd1fec53665b src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Aug 29 17:19:19 2023 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Aug 29 17:29:34 2023 +0200
@@ -117,7 +117,7 @@
     ml_statistics_step: Int = 1,
     component_repository: String = Components.static_component_repository,
     components_base: String = Components.dynamic_components_base,
-    clean_platforms: Option[List[Platform.Family.Value]] = None,
+    clean_platforms: Option[List[Platform.Family]] = None,
     clean_archives: Boolean = false,
     fresh: Boolean = false,
     hostname: String = "",
@@ -423,7 +423,7 @@
       var max_heap: Option[Int] = None
       var multicore_list = List(default_multicore)
       var isabelle_identifier = default_isabelle_identifier
-      var clean_platforms: Option[List[Platform.Family.Value]] = None
+      var clean_platforms: Option[List[Platform.Family]] = None
       var afp_partition = 0
       var clean_archives = false
       var component_repository = Components.static_component_repository
diff -r 67492b2a3a62 -r fd1fec53665b src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Tue Aug 29 17:19:19 2023 +0200
+++ b/src/Pure/Admin/build_release.scala	Tue Aug 29 17:29:34 2023 +0200
@@ -71,7 +71,7 @@
 """)
     }
 
-    def bundle_info(platform: Platform.Family.Value): Bundle_Info =
+    def bundle_info(platform: Platform.Family): Bundle_Info =
       platform match {
         case Platform.Family.linux_arm =>
           Bundle_Info(platform, "Linux (ARM)", dist_name + "_linux_arm.tar.gz")
@@ -82,7 +82,7 @@
   }
 
   sealed case class Bundle_Info(
-    platform: Platform.Family.Value,
+    platform: Platform.Family,
     platform_description: String,
     name: String
   ) {
@@ -150,7 +150,7 @@
 
   /* bundled components */
 
-  class Bundled(platform: Option[Platform.Family.Value] = None) {
+  class Bundled(platform: Option[Platform.Family] = None) {
     def detect(s: String): Boolean =
       s.startsWith("#bundled") && !s.startsWith("#bundled ")
 
@@ -186,7 +186,7 @@
         } yield bundled(line)).toList))
   }
 
-  def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = {
+  def get_bundled_components(dir: Path, platform: Platform.Family): (List[String], String) = {
     val Bundled = new Bundled(platform = Some(platform))
     val components =
       for { case Bundled(name) <- Components.Directory(dir).read_components() } yield name
@@ -195,8 +195,7 @@
     (components, jdk_component)
   }
 
-  def activate_components(
-    dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit = {
+  def activate_components(dir: Path, platform: Platform.Family, more_names: List[String]): Unit = {
     def contrib_name(name: String): String =
       Components.contrib(name = name).implode
 
@@ -219,7 +218,7 @@
 
   private def build_heaps(
     options: Options,
-    platform: Platform.Family.Value,
+    platform: Platform.Family,
     build_sessions: List[String],
     local_dir: Path,
     progress: Progress = new Progress,
@@ -275,7 +274,7 @@
   }
 
   def make_isabelle_app(
-    platform: Platform.Family.Value,
+    platform: Platform.Family,
     isabelle_target: Path,
     isabelle_name: String,
     jdk_component: String,
@@ -491,13 +490,13 @@
     }
   }
 
-  def default_platform_families: List[Platform.Family.Value] = Platform.Family.list0
+  def default_platform_families: List[Platform.Family] = Platform.Family.list0
 
   def build_release(
     options: Options,
     context: Release_Context,
     afp_rev: String = "",
-    platform_families: List[Platform.Family.Value] = default_platform_families,
+    platform_families: List[Platform.Family] = default_platform_families,
     more_components: List[Path] = Nil,
     website: Option[Path] = None,
     build_sessions: List[String] = Nil,
diff -r 67492b2a3a62 -r fd1fec53665b src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Aug 29 17:19:19 2023 +0200
+++ b/src/Pure/General/ssh.scala	Tue Aug 29 17:29:34 2023 +0200
@@ -493,7 +493,7 @@
 
     def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
 
-    def isabelle_platform_family: Platform.Family.Value =
+    def isabelle_platform_family: Platform.Family =
       Platform.Family.parse(isabelle_platform.ISABELLE_PLATFORM_FAMILY)
   }
 
diff -r 67492b2a3a62 -r fd1fec53665b src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Tue Aug 29 17:19:19 2023 +0200
+++ b/src/Pure/System/components.scala	Tue Aug 29 17:29:34 2023 +0200
@@ -35,7 +35,7 @@
 
   /* platforms */
 
-  private val family_platforms: Map[Platform.Family.Value, List[String]] =
+  private val family_platforms: Map[Platform.Family, List[String]] =
     Map(
       Platform.Family.linux_arm -> List("arm64-linux", "arm64_32-linux"),
       Platform.Family.linux -> List("x86_64-linux", "x86_64_32-linux"),
@@ -47,7 +47,7 @@
   private val platform_names: Set[String] =
     Set("x86-linux", "x86-cygwin") ++ family_platforms.iterator.flatMap(_._2)
 
-  def platform_purge(platforms: List[Platform.Family.Value]): String => Boolean = {
+  def platform_purge(platforms: List[Platform.Family]): String => Boolean = {
     val preserve =
       (for {
         family <- platforms.iterator
@@ -91,7 +91,7 @@
 
   def clean(
     component_dir: Path,
-    platforms: List[Platform.Family.Value] = Platform.Family.list,
+    platforms: List[Platform.Family] = Platform.Family.list,
     ssh: SSH.System = SSH.Local,
     progress: Progress = new Progress
   ): Unit = {
@@ -108,7 +108,7 @@
 
   def clean_base(
     base_dir: Path,
-    platforms: List[Platform.Family.Value] = Platform.Family.list,
+    platforms: List[Platform.Family] = Platform.Family.list,
     ssh: SSH.System = SSH.Local,
     progress: Progress = new Progress
   ): Unit = {
@@ -124,7 +124,7 @@
     name: String,
     target_dir: Option[Path] = None,
     copy_dir: Option[Path] = None,
-    clean_platforms: Option[List[Platform.Family.Value]] = None,
+    clean_platforms: Option[List[Platform.Family]] = None,
     clean_archives: Boolean = false,
     component_repository: String = Components.static_component_repository,
     ssh: SSH.System = SSH.Local,
diff -r 67492b2a3a62 -r fd1fec53665b src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Tue Aug 29 17:19:19 2023 +0200
+++ b/src/Pure/System/other_isabelle.scala	Tue Aug 29 17:29:34 2023 +0200
@@ -89,7 +89,7 @@
 
   def resolve_components(
     echo: Boolean = false,
-    clean_platforms: Option[List[Platform.Family.Value]] = None,
+    clean_platforms: Option[List[Platform.Family]] = None,
     clean_archives: Boolean = false,
     component_repository: String = Components.static_component_repository
   ): Unit = {
@@ -152,7 +152,7 @@
     other_settings: List[String] = init_components(),
     fresh: Boolean = false,
     echo: Boolean = false,
-    clean_platforms: Option[List[Platform.Family.Value]] = None,
+    clean_platforms: Option[List[Platform.Family]] = None,
     clean_archives: Boolean = false,
     component_repository: String = Components.static_component_repository
   ): Unit = {
diff -r 67492b2a3a62 -r fd1fec53665b src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Tue Aug 29 17:19:19 2023 +0200
+++ b/src/Pure/System/platform.scala	Tue Aug 29 17:29:34 2023 +0200
@@ -17,38 +17,42 @@
 
   def is_arm: Boolean = cpu_arch.startsWith("arm")
 
-  def family: Family.Value =
+  def family: Family =
     if (is_linux && is_arm) Family.linux_arm
     else 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_arm, linux, macos, windows = Value
-    val list0: List[Value] = List(linux, windows, macos)
-    val list: List[Value] = List(linux, linux_arm, windows, macos)
+  object Family {
+    val list0: List[Family] = List(Family.linux, Family.windows, Family.macos)
+    val list: List[Family] = List(Family.linux, Family.linux_arm, Family.windows, Family.macos)
 
-    def unapply(name: String): Option[Value] =
-      try { Some(withName(name)) }
-      catch { case _: NoSuchElementException => None }
+    def unapply(name: String): Option[Family] =
+      try { Some(Family.valueOf(name)) }
+      catch { case _: IllegalArgumentException => None }
 
-    def parse(name: String): Value =
+    def parse(name: String): Family =
       unapply(name) getOrElse error("Bad platform family: " + quote(name))
 
-    def standard(platform: Value): String =
-      if (platform == linux_arm) "arm64-linux"
-      else if (platform == linux) "x86_64-linux"
-      else if (platform == macos) "x86_64-darwin"
-      else if (platform == windows) "x86_64-cygwin"
-      else error("Bad platform family: " + quote(platform.toString))
+    val standard: Family => String =
+      {
+        case Family.linux_arm => "arm64-linux"
+        case Family.linux => "x86_64-linux"
+        case Family.macos => "x86_64-darwin"
+        case Family.windows => "x86_64-cygwin"
+      }
 
-    def native(platform: Value): String =
-      if (platform == macos) "arm64-darwin"
-      else if (platform == windows) "x86_64-windows"
-      else standard(platform)
+    val native: Family => String =
+      {
+        case Family.macos => "arm64-darwin"
+        case Family.windows => "x86_64-windows"
+        case platform => standard(platform)
+      }
   }
 
+  enum Family { case linux_arm, linux, macos, windows }
+
 
   /* platform identifiers */
 
diff -r 67492b2a3a62 -r fd1fec53665b src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala	Tue Aug 29 17:19:19 2023 +0200
+++ b/src/Pure/Tools/dotnet_setup.scala	Tue Aug 29 17:29:34 2023 +0200
@@ -11,7 +11,7 @@
   /* platforms */
 
   sealed case class Platform_Info(
-    family: Platform.Family.Value,
+    family: Platform.Family,
     name: String,
     os: String = "",
     arch: String = "x64",
diff -r 67492b2a3a62 -r fd1fec53665b src/Tools/VSCode/src/component_vscodium.scala
--- a/src/Tools/VSCode/src/component_vscodium.scala	Tue Aug 29 17:19:19 2023 +0200
+++ b/src/Tools/VSCode/src/component_vscodium.scala	Tue Aug 29 17:29:34 2023 +0200
@@ -58,7 +58,7 @@
   /* platform info */
 
   sealed case class Platform_Info(
-    platform: Platform.Family.Value,
+    platform: Platform.Family,
     download_template: String,
     build_name: String,
     env: List[String]
@@ -233,7 +233,7 @@
       .text.replaceAll("=", "")
   }
 
-  private val platform_infos: Map[Platform.Family.Value, Platform_Info] =
+  private val platform_infos: Map[Platform.Family, Platform_Info] =
     Iterator(
       Platform_Info(Platform.Family.linux, "linux-x64-{VERSION}.tar.gz", "VSCode-linux-x64",
         List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True")),
@@ -250,7 +250,7 @@
           "SHOULD_BUILD_MSI_NOUP=no")))
       .map(info => info.platform -> info).toMap
 
-  def the_platform_info(platform: Platform.Family.Value): Platform_Info =
+  def the_platform_info(platform: Platform.Family): Platform_Info =
     platform_infos.getOrElse(platform, error("No platform info for " + quote(platform.toString)))
 
   def linux_platform_info: Platform_Info =
@@ -259,7 +259,7 @@
 
   /* check system */
 
-  def check_system(platforms: List[Platform.Family.Value]): Unit = {
+  def check_system(platforms: List[Platform.Family]): Unit = {
     if (Platform.family != Platform.Family.linux) error("Not a Linux/x86_64 system")
 
     Isabelle_System.require_command("git")
@@ -301,11 +301,11 @@
 
   /* build vscodium */
 
-  def default_platforms: List[Platform.Family.Value] = Platform.Family.list
+  def default_platforms: List[Platform.Family] = Platform.Family.list
 
   def component_vscodium(
     target_dir: Path = Path.current,
-    platforms: List[Platform.Family.Value] = default_platforms,
+    platforms: List[Platform.Family] = default_platforms,
     progress: Progress = new Progress
   ): Unit = {
     check_system(platforms)