# HG changeset patch
# User wenzelm
# Date 1711557586 -3600
# Node ID a0f93621c332995496f2556062225bf761ddf055
# Parent  9b2f72f5a29ab48626785d8bce8587ca1c1f0828# Parent  30eb547bda4aadcd6507950fdff5755018a43966
merged

diff -r 9b2f72f5a29a -r a0f93621c332 NEWS
--- a/NEWS	Wed Mar 27 16:48:36 2024 +0100
+++ b/NEWS	Wed Mar 27 17:39:46 2024 +0100
@@ -259,14 +259,16 @@
 
 * The command-line tools "isabelle go_setup" and "isabelle go" /
 "isabelle gofmt" support the Go development environment. This works
-uniformly on all Isabelle OS platforms.
-
-Example:
+uniformly on all Isabelle OS platforms, separately or simultaneously.
+
+For example:
 
   isabelle go_setup
   isabelle go env
   isabelle go
 
+  isabelle go_setup -p all
+
 * Update to GHC stack 2.15.1 with support for all platforms, including
 ARM Linux and Apple Silicon.
 
diff -r 9b2f72f5a29a -r a0f93621c332 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Wed Mar 27 16:48:36 2024 +0100
+++ b/src/Pure/System/platform.scala	Wed Mar 27 17:39:46 2024 +0100
@@ -81,6 +81,19 @@
 
   /* platform info */
 
+  object Info {
+    val ALL = "all"
+
+    def check(infos: List[Info], spec: String): String = {
+      val specs = Library.distinct(ALL :: infos.map(_.family_name) ::: infos.map(_.platform))
+      if (specs.contains(spec)) spec
+      else {
+        error("Bad platform specification " + quote(spec) +
+          "\n  expected " + commas_quote(specs))
+      }
+    }
+  }
+
   trait Info {
     def platform: String
     override def toString: String = platform
@@ -94,16 +107,8 @@
     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))
-    }
+    def is(spec: String): Boolean =
+      Info.ALL == spec || platform == spec || family_name == spec
   }
 
 
diff -r 9b2f72f5a29a -r a0f93621c332 src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala	Wed Mar 27 16:48:36 2024 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala	Wed Mar 27 17:39:46 2024 +0100
@@ -30,8 +30,7 @@
         exec = "powershell -ExecutionPolicy ByPass",
         check = () => Isabelle_System.require_command("powershell", "-NoProfile -Command Out-Null")))
 
-  def check_platform_spec(spec: String): String =
-    Platform.check_spec(all_platforms, spec)
+  def check_platform(spec: String): String = Platform.Info.check(all_platforms, spec)
 
 
   /* dotnet download and setup */
@@ -51,7 +50,7 @@
     dry_run: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
-    platforms.foreach(check_platform_spec)
+    platforms.foreach(check_platform)
 
 
     /* component directory */
@@ -155,7 +154,7 @@
                  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,
+    -p PLATFORMS comma-separated list of platform specifications: "all" or
                  as family or formal name (default: """ + quote(default_platform) + """)
     -v           verbose
 
@@ -171,7 +170,7 @@
           "V:" -> (arg => version = arg),
           "f" -> (_ => force = true),
           "n" -> (_ => dry_run = true),
-          "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)),
+          "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform)),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
diff -r 9b2f72f5a29a -r a0f93621c332 src/Pure/Tools/go_setup.scala
--- a/src/Pure/Tools/go_setup.scala	Wed Mar 27 16:48:36 2024 +0100
+++ b/src/Pure/Tools/go_setup.scala	Wed Mar 27 17:39:46 2024 +0100
@@ -28,8 +28,7 @@
       Platform_Info("x86_64-linux", "linux_amd64"),
       Platform_Info("x86_64-windows", "windows_amd64"))
 
-  def check_platform_spec(spec: String): String =
-    Platform.check_spec(all_platforms, spec)
+  def check_platform(spec: String): String = Platform.Info.check(all_platforms, spec)
 
 
   /* Go download and setup */
@@ -48,7 +47,7 @@
     progress: Progress = new Progress,
     force: Boolean = false
   ): Unit = {
-    platforms.foreach(check_platform_spec)
+    platforms.foreach(check_platform)
 
 
     /* component directory */
@@ -149,7 +148,7 @@
     -U URL       download URL (default: """" + default_url + """")
     -V VERSION   version (default: """" + default_version + """")
     -f           force fresh installation of specified platforms
-    -p PLATFORMS comma-separated list of platform specifications,
+    -p PLATFORMS comma-separated list of platform specifications: "all" or
                  as family or formal name (default: """ + quote(default_platform) + """)
 
   Download the Go development environment and configure it as Isabelle
@@ -159,7 +158,7 @@
           "U:" -> (arg => base_url = arg),
           "V:" -> (arg => version = arg),
           "f" -> (_ => force = true),
-          "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)))
+          "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform)))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()