diff --git a/src/Pure/Admin/component_go.scala b/src/Pure/Admin/component_go.scala
--- a/src/Pure/Admin/component_go.scala
+++ b/src/Pure/Admin/component_go.scala
@@ -1,155 +1,152 @@
 /*  Title:      Pure/Admin/component_go.scala
     Author:     Makarius
 
 Build Isabelle component for Go: https://go.dev
 */
 
 package isabelle
 
 
 object Component_Go {
   /* platform information */
 
-  sealed case class Download_Platform(platform_name: String, go_platform: String) {
-    val platform_family: Platform.Family =
-      Platform.Family.from_platform(platform_name)
-
-    def platform_paths: List[String] =
-      List(platform_name, "pkg/tool/" + go_platform)
+  sealed case class Platform_Info(platform: String, go_platform: String)
+  extends Platform.Info {
+    def paths: List[String] = List(platform, "pkg/tool/" + go_platform)
 
     def download(base_url: String, version: String): String = {
-      val ext = if (platform_family == Platform.Family.windows) ".zip" else ".tar.gz"
+      val ext = if (is_windows) ".zip" else ".tar.gz"
       Url.append_path(base_url, "go" + version + "." + go_platform.replace("_", "-") + ext)
     }
   }
 
-  val platforms: List[Download_Platform] =
+  val all_platforms: List[Platform_Info] =
     List(
-      Download_Platform("arm64-darwin", "darwin_arm64"),
-      Download_Platform("arm64-linux", "linux_arm64"),
-      Download_Platform("x86_64-darwin", "darwin_amd64"),
-      Download_Platform("x86_64-linux", "linux_amd64"),
-      Download_Platform("x86_64-windows", "windows_amd64"))
+      Platform_Info("arm64-darwin", "darwin_arm64"),
+      Platform_Info("arm64-linux", "linux_arm64"),
+      Platform_Info("x86_64-darwin", "darwin_amd64"),
+      Platform_Info("x86_64-linux", "linux_amd64"),
+      Platform_Info("x86_64-windows", "windows_amd64"))
 
 
   /* build go */
 
   val default_url = "https://go.dev/dl"
   val default_version = "1.22.1"
 
   def build_go(
     base_url: String = default_url,
     version: String = default_version,
     target_dir: Path = Path.current,
     progress: Progress = new Progress
   ): Unit = {
     val component_dir =
       Components.Directory(target_dir + Path.basic("go-" + version)).create(progress = progress)
 
 
     /* download */
 
     Isabelle_System.with_tmp_dir("download") { download_dir =>
-      for (platform <- platforms.reverse) {
+      for (platform <- all_platforms.reverse) {
         val download = platform.download(base_url, version)
 
         val archive_name =
           Url.get_base_name(download) getOrElse
             error("Malformed download URL " + quote(download))
         val archive_path = download_dir + Path.basic(archive_name)
 
         Isabelle_System.download_file(download, archive_path, progress = progress)
         Isabelle_System.extract(archive_path, component_dir.path, strip = true)
 
-        val platform_dir = component_dir.path + Path.explode(platform.platform_name)
+        val platform_dir = component_dir.path + platform.path
         Isabelle_System.move_file(component_dir.bin, platform_dir)
       }
     }
 
     File.find_files(component_dir.path.file, pred = file => File.is_exe(file.getName)).
       foreach(file => File.set_executable(File.path(file)))
 
 
     /* isabelle tool */
 
     val isabelle_tool_dir = component_dir.path + Path.explode("isabelle_tool")
     Isabelle_System.make_directory(isabelle_tool_dir)
 
     for (tool <- List("go", "gofmt")) {
       val isabelle_tool = isabelle_tool_dir + Path.basic(tool)
       File.write(isabelle_tool,
 """#!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # DESCRIPTION: invoke """ + tool + """ within the Isabelle environment
 
 export GOROOT="$ISABELLE_GOROOT"
 exec "$ISABELLE_GOEXE/""" + tool + """" "$@"
 """)
       File.set_executable(isabelle_tool)
     }
 
 
     /* settings */
 
     component_dir.write_settings("""
 ISABELLE_GOROOT="$COMPONENT"
 ISABELLE_GOEXE="$ISABELLE_GOROOT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$ISABELLE_GOROOT/isabelle_tool"
 """)
 
 
     /* platform.props */
 
     File.write(component_dir.platform_props,
-      (for ((a, b) <- platforms.groupBy(_.platform_family).iterator)
-        yield a.toString + " = " + b.flatMap(_.platform_paths).mkString(" ")
+      (for ((a, b) <- all_platforms.groupBy(_.family_name).iterator)
+        yield a + " = " + b.flatMap(_.paths).mkString(" ")
       ).mkString("", "\n", "\n"))
 
 
     /* README */
 
     File.write(component_dir.README,
       """This distribution of Go has been assembled from official downloads from
 """ + base_url + """
 
 
         Makarius
         """ + Date.Format.date(Date.now()) + "\n")
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("component_go", "build component for Go", Scala_Project.here,
       { args =>
         var target_dir = Path.current
         var base_url = default_url
         var version = default_version
 
         val getopts = Getopts("""
 Usage: isabelle component_go [OPTIONS]
 
   Options are:
     -D DIR       target directory (default ".")
     -U URL       download URL (default: """" + default_url + """")
     -V VERSION   version (default: """" + default_version + """")
 
   Build component for Go development environment.
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
           "U:" -> (arg => base_url = arg),
           "V:" -> (arg => version = arg))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress()
 
         build_go(base_url = base_url, version = version, target_dir = target_dir,
           progress = progress)
       })
 }
diff --git a/src/Pure/System/platform.scala b/src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala
+++ b/src/Pure/System/platform.scala
@@ -1,95 +1,123 @@
 /*  Title:      Pure/System/platform.scala
     Author:     Makarius
 
 System platform identification.
 */
 
 package isabelle
 
 
 object Platform {
   /* platform family */
 
   val is_windows: Boolean = isabelle.setup.Environment.is_windows()
   val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
   val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
   val is_unix: Boolean = is_linux || is_macos
 
   def is_arm: Boolean = cpu_arch.startsWith("arm")
 
   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 {
     val list: List[Family] = List(Family.linux, Family.linux_arm, Family.windows, Family.macos)
 
     def unapply(name: String): Option[Family] =
       try { Some(Family.valueOf(name)) }
       catch { case _: IllegalArgumentException => None }
 
     def parse(name: String): Family =
       unapply(name) getOrElse error("Bad platform family: " + quote(name))
 
     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"
       }
 
     val native: Family => String =
       {
         case Family.macos => "arm64-darwin"
         case Family.windows => "x86_64-windows"
         case platform => standard(platform)
       }
 
     def from_platform(platform: String): Family =
       list.find(family => platform == standard(family) || platform == native(family))
         .getOrElse(error("Bad platform " + quote(platform)))
   }
 
   enum Family { case linux_arm, linux, macos, windows }
 
 
   /* platform identifiers */
 
   private val X86_64 = """amd64|x86_64""".r
   private val Arm64 = """arm64|aarch64""".r
 
   def cpu_arch: String =
     System.getProperty("os.arch", "") match {
       case X86_64() => "x86_64"
       case Arm64() => "arm64"
       case _ => error("Failed to determine CPU architecture")
     }
 
   def os_name: String =
     family match {
       case Family.linux_arm => "linux"
       case Family.macos => "darwin"
       case _ => family.toString
     }
 
   lazy val jvm_platform: String = cpu_arch + "-" + os_name
 
 
+  /* platform info */
+
+  trait Info {
+    def platform: String
+    override def toString: String = platform
+    def path: Path = Path.explode(platform)
+
+    val family: Family = Family.from_platform(platform)
+    def family_name: String = family.toString
+
+    def is_linux_arm: Boolean = family == Family.linux_arm
+    def is_linux: Boolean = family == Family.linux
+    def is_macos: Boolean = family == Family.macos
+    def is_windows: Boolean = family == Family.windows
+
+    def is(spec: String): Boolean = platform == spec || family_name == spec
+  }
+
+  def check_spec(infos: List[Info], spec: String): String = {
+    val specs = Library.distinct(infos.map(_.family_name) ::: infos.map(_.platform))
+    if (specs.contains(spec)) spec
+    else {
+      error("Bad platform specification " + quote(spec) +
+        "\n  expected " + commas_quote(specs))
+    }
+  }
+
+
   /* JVM version */
 
   private val Version = """1\.(\d+)\.0_(\d+)""".r
   lazy val jvm_version: String =
     System.getProperty("java.version") match {
       case Version(a, b) => a + "u" + b
       case a => a
     }
 
 
   /* JVM name */
 
   val jvm_name: String = System.getProperty("java.vm.name", "")
 }
diff --git a/src/Pure/Tools/dotnet_setup.scala b/src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala
+++ b/src/Pure/Tools/dotnet_setup.scala
@@ -1,204 +1,192 @@
 /*  Title:      Pure/Tools/dotnet_setup.scala
     Author:     Makarius
 
 Dynamic setup of dotnet component.
 */
 
 package isabelle
 
 
 object Dotnet_Setup {
   /* platforms */
 
   sealed case class Platform_Info(
-    name: String,
+    platform: String,
     os: String = "",
     arch: String = "x64",
     ext: String = "sh",
     exec: String = "bash",
     check: () => Unit = () => ()
-  ) {
-    val family: Platform.Family = Platform.Family.from_platform(name)
-  }
+  ) extends Platform.Info
 
-  private val all_platforms =
+  val all_platforms: List[Platform_Info] =
     List(
       Platform_Info("arm64-linux", os = "linux", arch = "arm64"),
       Platform_Info("x86_64-linux", os = "linux"),
       Platform_Info("arm64-darwin", os = "osx", arch = "arm64"),
       Platform_Info("x86_64-darwin", os = "osx"),
       Platform_Info("x86_64-windows",
         ext = "ps1",
         exec = "powershell -ExecutionPolicy ByPass",
         check = () => Isabelle_System.require_command("powershell", "-NoProfile -Command Out-Null")))
 
-  def check_platform_spec(spec: String): String = {
-    val all_specs =
-      Library.distinct(all_platforms.map(_.family.toString) ::: all_platforms.map(_.name))
-    if (all_specs.contains(spec)) spec
-    else {
-      error("Bad platform specification " + quote(spec) +
-        "\n  expected " + commas_quote(all_specs))
-    }
-  }
+  def check_platform_spec(spec: String): String =
+    Platform.check_spec(all_platforms, spec)
 
 
   /* dotnet download and setup */
 
   def default_platform: String = {
     val self = Isabelle_Platform.self
     proper_string(self.ISABELLE_WINDOWS_PLATFORM64).getOrElse(
       proper_string(self.ISABELLE_APPLE_PLATFORM64).getOrElse(
         self.ISABELLE_PLATFORM64))
   }
 
   def default_target_dir: Path = Components.default_components_base
   def default_install_url: String = "https://dot.net/v1/dotnet-install"
   def default_version: String = Isabelle_System.getenv_strict("ISABELLE_DOTNET_VERSION")
 
   def dotnet_setup(
     platform_spec: String = default_platform,
     target_dir: Path = default_target_dir,
     install_url: String = default_install_url,
     version: String = default_version,
     force: Boolean = false,
     dry_run: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
     check_platform_spec(platform_spec)
 
-    for {
-      platform <- all_platforms
-      if platform.family.toString == platform_spec || platform.name == platform_spec
-    } {
+    for (platform <- all_platforms if platform.is(platform_spec)) {
       progress.expose_interrupt()
 
 
       /* component directory */
 
       val component_dir =
         Components.Directory(
           target_dir + Path.explode(if (version.isEmpty) "dotnet-latest" else "dotnet-" + version))
 
       if (!dry_run) {
         progress.echo("Component " + component_dir)
         Isabelle_System.make_directory(component_dir.etc)
 
         component_dir.write_settings("""
 ISABELLE_DOTNET_ROOT="$COMPONENT"
 
 if [ -n "$ISABELLE_WINDOWS_PLATFORM64" -a -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_WINDOWS_PLATFORM64" ]; then
   ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_WINDOWS_PLATFORM64/dotnet.exe"
 elif [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_APPLE_PLATFORM64" ]; then
   ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_APPLE_PLATFORM64/dotnet"
 elif [ -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_PLATFORM64" ]; then
   ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_PLATFORM64/dotnet"
 fi
 
 DOTNET_CLI_TELEMETRY_OPTOUT="true"
 DOTNET_CLI_HOME="$(platform_path "$ISABELLE_HOME_USER/dotnet")"
 """)
 
         File.write(component_dir.README,
           """This installation of Dotnet has been produced via "isabelle dotnet_setup".
 
 
         Makarius
         """ + Date.Format.date(Date.now()) + "\n")
 
         for (old <- proper_string(Isabelle_System.getenv("ISABELLE_DOTNET_ROOT"))) {
           Components.update_components(false, Path.explode(old))
         }
 
         Components.update_components(true, component_dir.path)
       }
 
 
       /* platform directory */
 
       Isabelle_System.with_tmp_file("install", ext = platform.ext) { install =>
         Isabelle_System.download_file(install_url + "." + platform.ext, install)
 
-        val platform_dir = component_dir.path + Path.explode(platform.name)
+        val platform_dir = component_dir.path + platform.path
         if (platform_dir.is_dir && !force) {
-          progress.echo_warning("Platform " + platform.name + " already installed")
+          progress.echo_warning("Platform " + platform + " already installed")
         }
         else {
-          progress.echo("Platform " + platform.name + " ...")
+          progress.echo("Platform " + platform + " ...")
           platform.check()
           if (platform_dir.is_dir && force) Isabelle_System.rm_tree(platform_dir)
           val script =
             platform.exec + " " + File.bash_platform_path(install) +
               if_proper(version, " -Version " + Bash.string(version)) +
               " -Architecture " + Bash.string(platform.arch) +
               if_proper(platform.os, " -OS " + Bash.string(platform.os)) +
-              " -InstallDir " + Bash.string(platform.name) +
+              " -InstallDir " + File.bash_path(platform.path) +
               (if (dry_run) " -DryRun" else "") +
               " -NoPath"
           progress.bash(script, echo = progress.verbose,
             cwd = if (dry_run) null else component_dir.path.file).check
           for (exe <- File.find_files(platform_dir.file, pred = _.getName.endsWith(".exe"))) {
             File.set_executable(File.path(exe))
           }
         }
       }
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("dotnet_setup", "dynamic setup of dotnet component (for Fsharp)",
       Scala_Project.here,
       { args =>
 
         var target_dir = default_target_dir
         var install_url = default_install_url
         var version = default_version
         var force = false
         var dry_run = false
         var platforms = List(default_platform)
         var verbose = false
 
         val getopts = Getopts("""
 Usage: isabelle dotnet_setup [OPTIONS]
 
   Options are:
     -D DIR       target directory (default: """ + default_target_dir.expand + """)
     -I URL       URL for install script without extension
                  (default: """ + quote(default_install_url) + """)
     -V VERSION   version (empty means "latest",
                  default: ISABELLE_DOTNET_VERSION=""" + quote(default_version) + """)
     -f           force fresh installation of specified platforms
     -n           dry run: try download without installation
     -p PLATFORMS comma-separated list of platform specifications,
                  as family or formal name (default: """ + quote(default_platform) + """)
     -v           verbose
 
   Download the Dotnet / Fsharp platform and configure it as Isabelle component.
 
   See also:
     https://fsharp.org
     https://learn.microsoft.com/en-us/dotnet/core/tools/dotnet-install-script
     https://learn.microsoft.com/en-us/dotnet/core/tools/telemetry
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
           "I:" -> (arg => install_url = arg),
           "V:" -> (arg => version = arg),
           "f" -> (_ => force = true),
           "n" -> (_ => dry_run = true),
           "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress(verbose = verbose)
 
         for (platform <- platforms) {
           dotnet_setup(platform_spec = platform, target_dir = target_dir, install_url = install_url,
             version = version, force = force, dry_run = dry_run, progress = progress)
         }
       })
 }