# HG changeset patch
# User wenzelm
# Date 1646494079 -3600
# Node ID 419781ac89bf0b6f825adb711aa2f42726d77d17
# Parent  8c09e1f82f8162d6582e73069400f0764671255d
misc tuning and clarification;

diff -r 8c09e1f82f81 -r 419781ac89bf src/Pure/Admin/build_vscodium.scala
--- a/src/Pure/Admin/build_vscodium.scala	Sat Mar 05 14:31:29 2022 +0100
+++ b/src/Pure/Admin/build_vscodium.scala	Sat Mar 05 16:27:59 2022 +0100
@@ -18,13 +18,41 @@
 
   lazy val version: String = Isabelle_System.getenv_strict("ISABELLE_VSCODE_VERSION")
   val vscodium_repository = "https://github.com/VSCodium/vscodium.git"
+  val vscodium_download = "https://github.com/VSCodium/vscodium/releases/download"
+
+  def vscodium_exe(dir: Path): Path = dir + Path.explode("bin/codium")
 
 
   /* platform info */
 
   sealed case class Platform_Info(
-    platform: Platform.Family.Value, build_name: String, env: List[String])
+    platform: Platform.Family.Value,
+    download_template: String,
+    build_name: String,
+    env: List[String])
   {
+    def download_name: String = "VSCodium-" + download_template.replace("{VERSION}", version)
+    def download_zip: Boolean = download_name.endsWith(".zip")
+
+    def download(dir: Path, progress: Progress = new Progress): Unit =
+    {
+      if (download_zip) Isabelle_System.require_command("unzip", test = "-h")
+
+      Isabelle_System.with_tmp_file("download")(download_file =>
+      {
+        Isabelle_System.download_file(vscodium_download + "/" + version + "/" + download_name,
+          download_file, progress = progress)
+
+        progress.echo("Unpacking " + dir.expand)
+        if (download_zip) {
+          Isabelle_System.bash("unzip -x " + File.bash_path(download_file), cwd = dir.file).check
+        }
+        else {
+          Isabelle_System.gnutar("-xzf " + File.bash_path(download_file), dir = dir).check
+        }
+      })
+    }
+
     def platform_dir(dir: Path): Path =
     {
       val platform_name =
@@ -35,16 +63,21 @@
 
     def build_dir(dir: Path): Path = dir + Path.explode(build_name)
 
-    def environment: String =
+    def build_environment: String =
       (("MS_TAG=" + Bash.string(version)) :: "SHOULD_BUILD=yes" :: "VSCODE_ARCH=x64" :: env)
         .map(s => "export " + s + "\n").mkString
 
-    def patch_resources(base_dir: Path): Unit =
+    def resources_dir(dir: Path): Path =
     {
       val resources =
         if (platform == Platform.Family.macos) "VSCodium.app/Contents/Resources"
         else "resources"
-      val dir = platform_dir(base_dir) + Path.explode(resources)
+      dir + Path.explode(resources)
+    }
+
+    def patch_resources(dir0: Path): Unit =
+    {
+      val dir = resources_dir(dir0)
 
       HTML.init_fonts(dir + Path.explode("app/out/vs/base/browser/ui"))
 
@@ -61,6 +94,28 @@
         else line)
       }
     }
+
+    def setup_executables(dir: Path): Unit =
+    {
+      val exe = vscodium_exe(dir)
+      Isabelle_System.make_directory(exe.dir)
+
+      platform match {
+        case Platform.Family.macos =>
+          File.write(exe, macos_exe)
+          File.set_executable(exe, true)
+        case Platform.Family.windows =>
+          val files1 = File.find_files(exe.dir.file)
+          val files2 = File.find_files(dir.file, pred = file =>
+            {
+              val name = file.getName
+              name.endsWith(".dll") || name.endsWith(".exe") || name.endsWith(".node")
+            })
+          for (file <- files1 ::: files2) File.set_executable(File.path(file), true)
+          Isabelle_System.bash("chmod -R o-w " + File.bash_path(dir))
+        case _ =>
+      }
+    }
   }
 
   // see https://github.com/microsoft/vscode/blob/main/build/gulpfile.vscode.js
@@ -73,15 +128,15 @@
       .text.replaceAll("=", "")
   }
 
-  private val platform_info: Map[Platform.Family.Value, Platform_Info] =
+  private val platform_infos: Map[Platform.Family.Value, Platform_Info] =
     Iterator(
-      Platform_Info(Platform.Family.linux, "VSCode-linux-x64",
+      Platform_Info(Platform.Family.linux, "linux-x64-{VERSION}.tar.gz", "VSCode-linux-x64",
         List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True")),
-      Platform_Info(Platform.Family.linux_arm, "VSCode-linux-arm64",
+      Platform_Info(Platform.Family.linux_arm, "linux-arm64-{VERSION}.tar.gz", "VSCode-linux-arm64",
         List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True", "VSCODE_ARCH=arm64")),
-      Platform_Info(Platform.Family.macos, "VSCode-darwin-x64",
+      Platform_Info(Platform.Family.macos, "darwin-x64-{VERSION}.zip", "VSCode-darwin-x64",
         List("OS_NAME=osx")),
-      Platform_Info(Platform.Family.windows, "VSCode-win32-x64",
+      Platform_Info(Platform.Family.windows, "win32-x64-{VERSION}.zip", "VSCode-win32-x64",
         List("OS_NAME=windows",
           "SHOULD_BUILD_ZIP=no",
           "SHOULD_BUILD_EXE_SYS=no",
@@ -90,6 +145,9 @@
           "SHOULD_BUILD_MSI_NOUP=no")))
       .map(info => info.platform -> info).toMap
 
+  def the_platform_info(platform: Platform.Family.Value): Platform_Info =
+    platform_infos.getOrElse(platform, error("No platform info for " + quote(platform.toString)))
+
 
   /* check system */
 
@@ -106,6 +164,9 @@
     if (platforms.contains(Platform.Family.windows)) {
       Isabelle_System.require_command("wine")
     }
+    if (platforms.exists(platform => the_platform_info(platform).download_zip)) {
+      Isabelle_System.require_command("unzip", test = "-h")
+    }
   }
 
 
@@ -113,8 +174,6 @@
 
   def default_platforms: List[Platform.Family.Value] = Platform.Family.list
 
-  private def vscodium_exe(dir: Path): Path = dir + Path.explode("bin/codium")
-
   def macos_exe: String =
 """#!/usr/bin/env bash
 
@@ -127,12 +186,6 @@
 exit $?
 """
 
-  def is_windows_exe(file: JFile): Boolean =
-  {
-    val name = file.getName
-    name.endsWith(".dll") || name.endsWith(".exe") || name.endsWith(".node")
-  }
-
   def build_vscodium(
     target_dir: Path = Path.current,
     platforms: List[Platform.Family.Value] = default_platforms,
@@ -152,15 +205,14 @@
     /* build */
 
     for (platform <- platforms) {
-      val info =
-        platform_info.getOrElse(platform, error("No platform info for " + quote(platform.toString)))
+      val platform_info = the_platform_info(platform)
 
       progress.echo("Building " + platform + " ...")
 
       Isabelle_System.with_tmp_dir("vscodium")(vscodium_dir =>
       {
         def execute(lines: String*): Unit =
-          progress.bash(("set -e" :: info.environment :: lines.toList).mkString("\n"),
+          progress.bash(("set -e" :: platform_info.build_environment :: lines.toList).mkString("\n"),
             cwd = vscodium_dir.file, echo = verbose).check
 
         execute(
@@ -177,26 +229,12 @@
 
         execute("./build.sh")
 
-        val platform_dir = info.platform_dir(component_dir)
-        Isabelle_System.copy_dir(info.build_dir(vscodium_dir), platform_dir)
         Isabelle_System.copy_file(vscodium_dir + Path.explode("LICENSE"), component_dir)
 
-        info.patch_resources(component_dir)
-
-        val exe = vscodium_exe(platform_dir)
-        Isabelle_System.make_directory(exe.dir)
-
-        platform match {
-          case Platform.Family.macos =>
-            File.write(exe, macos_exe)
-            File.set_executable(exe, true)
-          case Platform.Family.windows =>
-            val files1 = File.find_files(exe.dir.file)
-            val files2 = File.find_files(platform_dir.file, pred = is_windows_exe)
-            for (file <- files1 ::: files2) File.set_executable(File.path(file), true)
-            Isabelle_System.bash("chmod -R o-w " + File.bash_path(platform_dir))
-          case _ =>
-        }
+        val platform_dir = platform_info.platform_dir(component_dir)
+        Isabelle_System.copy_dir(platform_info.build_dir(vscodium_dir), platform_dir)
+        platform_info.patch_resources(platform_dir)
+        platform_info.setup_executables(platform_dir)
       })
     }
 
diff -r 8c09e1f82f81 -r 419781ac89bf src/Tools/VSCode/src/vscode_setup.scala
--- a/src/Tools/VSCode/src/vscode_setup.scala	Sat Mar 05 14:31:29 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Sat Mar 05 16:27:59 2022 +0100
@@ -20,25 +20,19 @@
   def vscode_home: Path = Path.variable("ISABELLE_VSCODE_HOME")
   def vscode_settings: Path = Path.variable("ISABELLE_VSCODE_SETTINGS")
   def vscode_settings_user: Path = vscode_settings + Path.explode("user-data/User/settings.json")
-  def vscode_version: String = Isabelle_System.getenv_strict("ISABELLE_VSCODE_VERSION")
   def vscode_workspace: Path = Path.variable("ISABELLE_VSCODE_WORKSPACE")
+  def version: String = Build_VSCodium.version
 
   def vscodium_home: Path = Path.variable("ISABELLE_VSCODIUM_HOME")
   def vscodium_home_ok(): Boolean =
     try { vscodium_home.is_dir }
     catch { case ERROR(_) => false }
 
-  def exe_path(dir: Path): Path = dir + Path.explode("bin/codium")
-
-  def vscode_installation(version: String, platform: Platform.Family.Value): (Boolean, Path) =
+  def vscode_installation(info: Build_VSCodium.Platform_Info): (Boolean, Path) =
   {
-    val platform_name =
-      if (platform == Platform.Family.windows) Platform.Family.native(platform)
-      else Platform.Family.standard(platform)
     val install_dir =
-      vscode_settings + Path.basic("installation") +
-        Path.basic(version) + Path.basic(platform_name)
-    val install_ok = exe_path(install_dir).is_file
+      info.platform_dir(vscode_settings + Path.basic("installation") + Path.basic(version))
+    val install_ok = Build_VSCodium.vscodium_exe(install_dir).is_file
     (install_ok, install_dir)
   }
 
@@ -98,7 +92,6 @@
 
   /* vscode setup */
 
-  val default_download_url: String = "https://github.com/VSCodium/vscodium/releases/download"
   def default_platform: Platform.Family.Value = Platform.family
 
   private val init_settings = """  {
@@ -117,14 +110,13 @@
 
   def vscode_setup(
     check: Boolean = false,
-    download_url: String = default_download_url,
-    version: String = vscode_version,
     platform: Platform.Family.Value = default_platform,
     quiet: Boolean = false,
     fresh: Boolean = false,
     progress: Progress = new Progress): Unit =
   {
-    val (install_ok, install_dir) = vscode_installation(version, platform)
+    val platform_info = Build_VSCodium.the_platform_info(platform)
+    val (install_ok, install_dir) = vscode_installation(platform_info)
 
     if (!vscode_settings_user.is_file) {
       Isabelle_System.make_directory(vscode_settings_user.dir)
@@ -150,56 +142,10 @@
         progress.echo_warning("Isabelle/VSCode installation already present: " + install_dir.expand)
       }
       if (!install_ok || fresh) {
-        val download_name =
-        {
-          val a = "VSCodium"
-          val (b, c) =
-            platform match {
-              case Platform.Family.linux_arm => ("linux-arm64", "tar.gz")
-              case Platform.Family.linux => ("linux-x64", "tar.gz")
-              case Platform.Family.macos => ("darwin-x64", "zip")
-              case Platform.Family.windows => ("win32-x64", "zip")
-            }
-          a + "-" + b + "-" + version + "." + c
-        }
-        val is_zip = download_name.endsWith(".zip")
-        if (is_zip) Isabelle_System.require_command("unzip", test = "-h")
-
         Isabelle_System.make_directory(install_dir)
-        val exe = exe_path(install_dir)
-
-        Isabelle_System.with_tmp_file("download")(download =>
-        {
-          Isabelle_System.download_file(download_url + "/" + version + "/" + download_name,
-            download, progress = if (quiet) new Progress else progress)
-          if (!quiet) progress.echo("Installing " + install_dir.expand)
-          if (is_zip) {
-            Isabelle_System.bash("unzip -x " + File.bash_path(download),
-              cwd = install_dir.file).check
-          }
-          else {
-            Isabelle_System.gnutar("-xzf " + File.bash_path(download),
-              dir = install_dir).check
-          }
-
-          platform match {
-            case Platform.Family.macos =>
-              Isabelle_System.make_directory(exe.dir)
-              File.write(exe, Build_VSCodium.macos_exe)
-              File.set_executable(exe, true)
-            case Platform.Family.windows =>
-              val files1 = File.find_files(exe.dir.file)
-              val files2 = File.find_files(install_dir.file, pred = Build_VSCodium.is_windows_exe)
-              for (file <- files1 ::: files2) File.set_executable(File.path(file), true)
-            case _ =>
-          }
-
-          patch_resources(
-            if (platform == Platform.Family.macos) {
-              install_dir + Path.explode("VSCodium.app/Contents/Resources")
-            }
-            else install_dir + Path.explode("resources"))
-        })
+        platform_info.download(install_dir, progress = if (quiet) new Progress else progress)
+        platform_info.patch_resources(install_dir)
+        platform_info.setup_executables(install_dir)
       }
     }
   }
@@ -212,8 +158,6 @@
       Scala_Project.here, args =>
     {
       var check = false
-      var download_url = default_download_url
-      var version = vscode_version
       var fresh = false
       var platforms = List(default_platform)
       var quiet = false
@@ -223,9 +167,6 @@
 
   Options are:
     -C           check and print installation directory
-    -U URL       download URL
-                 (default: """" + default_download_url + """")
-    -V VERSION   version (default: """" + vscode_version + """")
     -f           force fresh installation
     -p NAMES     platform families: comma-separated names
                  (""" + commas_quote(Platform.Family.list.map(_.toString)) + """, default: """ +
@@ -240,8 +181,6 @@
   The following initial settings are provided for a fresh installation:
 """ + init_settings,
         "C" -> (_ => check = true),
-        "U:" -> (arg => download_url = arg),
-        "V:" -> (arg => version = arg),
         "f" -> (_ => fresh = true),
         "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)),
         "q" -> (_ => quiet = true))
@@ -251,8 +190,7 @@
 
       val progress = new Console_Progress()
       for (platform <- platforms) {
-        vscode_setup(check = check, download_url = download_url, version = version,
-          platform = platform, quiet = quiet, fresh = fresh, progress = progress)
+        vscode_setup(check = check, platform = platform, quiet = quiet, fresh = fresh, progress = progress)
       }
     })
 }