--- 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.
--- 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
}
--- 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)
--- 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()