# HG changeset patch
# User wenzelm
# Date 1645180470 -3600
# Node ID 32ebb38154e7eb5a2531e546690c1fb0d2d5275c
# Parent  f3fcc7c5a0db9c9c6054e94cb86a258f7e85b495
clarified options;

diff -r f3fcc7c5a0db -r 32ebb38154e7 src/Tools/VSCode/src/vscode_setup.scala
--- a/src/Tools/VSCode/src/vscode_setup.scala	Thu Feb 17 19:42:16 2022 +0000
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Fri Feb 18 11:34:30 2022 +0100
@@ -17,7 +17,6 @@
   def vscode_home: Path = Path.variable("ISABELLE_VSCODE_HOME")
   def vscode_settings: Path = Path.variable("ISABELLE_VSCODE_SETTINGS")
   def vscode_version: String = Isabelle_System.getenv_strict("ISABELLE_VSCODE_VERSION")
-  def vscode_platform: Platform.Family.Value = Platform.family
 
   def vscode_installation(version: String, platform: Platform.Family.Value): (Boolean, Path) =
     {
@@ -35,6 +34,7 @@
   /* vscode setup */
 
   val default_download_url: String = "https://github.com/VSCodium/vscodium/releases/download"
+  def default_platform: Platform.Family.Value = Platform.family
 
   def download_name(version: String, platform: Platform.Family.Value): String =
   {
@@ -53,7 +53,7 @@
     check: Boolean = false,
     download_url: String = default_download_url,
     version: String = vscode_version,
-    platform: Platform.Family.Value = vscode_platform,
+    platform: Platform.Family.Value = default_platform,
     verbose: Boolean = false,
     progress: Progress = new Progress): Unit =
   {
@@ -110,7 +110,7 @@
       var check = false
       var download_url = default_download_url
       var version = vscode_version
-      var platform = vscode_platform
+      var platforms = List(default_platform)
       var verbose = false
 
       val getopts = Getopts("""
@@ -121,9 +121,10 @@
     -U URL       download URL
                  (default: """" + default_download_url + """")
     -V VERSION   version (default: """" + vscode_version + """")
-    -p NAME      platform family: """ + commas_quote(Platform.Family.list.map(_.toString)) + """
-                 (default: """ + quote(vscode_platform.toString) + """)
-    -v           verbose
+    -p NAMES     platform families: comma-separated names
+                 (""" + commas_quote(Platform.Family.list.map(_.toString)) + """, default: """ +
+        quote(default_platform.toString) + """)
+    -v           verbose mode
 
   Maintain local installation of VSCode, see also https://vscodium.com
 
@@ -133,14 +134,16 @@
         "C" -> (_ => check = true),
         "U:" -> (arg => download_url = arg),
         "V:" -> (arg => version = arg),
-        "p:" -> (arg => platform = Platform.Family.parse(arg)),
+        "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)),
         "v" -> (_ => verbose = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress()
-      vscode_setup(check = check, download_url = download_url, version = version,
-        platform = platform, verbose = verbose, progress = progress)
+      for (platform <- platforms) {
+        vscode_setup(check = check, download_url = download_url, version = version,
+          platform = platform, verbose = verbose, progress = progress)
+      }
     })
 }