clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode;

--- a/lib/Tools/vscode	Wed Mar 09 23:05:07 2022 +0100
+++ b/lib/Tools/vscode	Thu Mar 10 11:56:38 2022 +0100
@@ -2,10 +2,11 @@
 #
 # Author: Makarius
 #
-# DESCRIPTION: run Isabelle/VSCode using local VSCodium installation
+# DESCRIPTION: run Isabelle/VSCode (requires "vscodium-X.YY.Z" component)
 
-DIR="$(isabelle vscode_setup -C)" || exit "$?"
-exec "$DIR/bin/codium" \
+isabelle vscode_setup || exit "$?"
+
+exec "$ISABELLE_VSCODIUM_HOME/bin/codium" \
   --locale en-US \
   --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \
   --extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \

--- a/src/Tools/VSCode/src/vscode_setup.scala	Wed Mar 09 23:05:07 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Thu Mar 10 11:56:38 2022 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Tools/VSCode/src/vscode_setup.scala
     Author:     Makarius
 
-Setup VSCode from VSCodium distribution.
+Provide user configuration for Isabelle/VSCode.
 */
 
 package isabelle.vscode
@@ -9,68 +9,13 @@
 
 import isabelle._
 
-import java.security.MessageDigest
-import java.util.Base64
-
 
 object VSCode_Setup
 {
-  /* global resources */
-
-  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 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 vscode_installation(info: Build_VSCodium.Platform_Info): (Boolean, Path) =
-  {
-    val install_dir =
-      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)
-  }
-
-
-  /* patch resources */
-
-  // see https://github.com/microsoft/vscode/blob/main/build/gulpfile.vscode.js
-  // function computeChecksum(filename)
-
-  def file_checksum(path: Path): String =
-  {
-    val digest = MessageDigest.getInstance("MD5")
-    digest.update(Bytes.read(path).array)
-    Bytes(Base64.getEncoder.encode(digest.digest()))
-      .text.replaceAll("=", "")
-  }
-
-  def patch_resources(dir: Path): Unit =
-  {
-    HTML.init_fonts(dir + Path.explode("app/out/vs/base/browser/ui"))
-
-    val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css")
-    val checksum1 = file_checksum(workbench_css)
-    File.append(workbench_css, "\n\n" + HTML.fonts_css_dir(prefix = "../base/browser/ui"))
-    val checksum2 = file_checksum(workbench_css)
-
-    val file_name = workbench_css.file_name
-    File.change_lines(dir + Path.explode("app/product.json")) { _.map(line =>
-      if (line.containsSlice(file_name) && line.contains(checksum1)) {
-        line.replace(checksum1, checksum2)
-      }
-      else line)
-    }
-  }
-
-
   /* vscode setup */
 
-  def default_platform: Platform.Family.Value = Platform.family
+  def vscode_settings_user: Path =
+    Path.explode("$ISABELLE_VSCODE_SETTINGS/user-data/User/settings.json")
 
   private val init_settings = """  {
     "editor.fontFamily": "'Isabelle DejaVu Sans Mono'",
@@ -86,87 +31,36 @@
   }
 """
 
-  def vscode_setup(
-    check: Boolean = false,
-    platform: Platform.Family.Value = default_platform,
-    quiet: Boolean = false,
-    fresh: Boolean = false,
-    progress: Progress = new Progress): Unit =
+  def vscode_setup(): Unit =
   {
-    val platform_info = Build_VSCodium.the_platform_info(platform)
-    val (install_ok, install_dir) = vscode_installation(platform_info)
+    if (Isabelle_System.getenv("ISABELLE_VSCODIUM_HOME").isEmpty) {
+      error("""Missing $ISABELLE_VSCODIUM_HOME: proper vscodium-X.YY.Z component required""")
+    }
 
     if (!vscode_settings_user.is_file) {
       Isabelle_System.make_directory(vscode_settings_user.dir)
       File.write(vscode_settings_user, init_settings)
     }
-
-    if (check) {
-      if (vscodium_home_ok()) {
-        progress.echo(vscodium_home.expand.implode)
-      }
-      else if (install_ok) {
-        progress.echo(install_dir.expand.implode)
-      }
-      else {
-        error("Bad Isabelle/VSCode installation: " + install_dir.expand +
-          "\n(use \"isabelle vscode_setup\" for download and installation)")
-      }
-    }
-    else {
-      if (install_ok) {
-        progress.echo_warning("Isabelle/VSCode installation already present: " + install_dir.expand)
-      }
-      if (!install_ok || fresh) {
-        Isabelle_System.make_directory(install_dir)
-        platform_info.download(install_dir, progress = if (quiet) new Progress else progress)
-        platform_info.patch_resources(install_dir)
-        platform_info.setup_executables(install_dir)
-      }
-    }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("vscode_setup", "setup VSCode from VSCodium distribution",
+    Isabelle_Tool("vscode_setup", "provide user configuration for Isabelle/VSCode",
       Scala_Project.here, args =>
     {
-      var check = false
-      var fresh = false
-      var platforms = List(default_platform)
-      var quiet = false
-
       val getopts = Getopts("""
-Usage: vscode_setup [OPTIONS]
+Usage: vscode_setup
 
-  Options are:
-    -C           check and print installation directory
-    -f           force fresh installation
-    -p NAMES     platform families: comma-separated names
-                 (""" + commas_quote(Platform.Family.list.map(_.toString)) + """, default: """ +
-        quote(default_platform.toString) + """)
-    -q           quiet mode
-
-  Maintain local installation of VSCode, see also https://vscodium.com
-
-  Option -C checks the existing installation (without download), and
-  prints its directory location.
+  Provide user configuration for Isabelle/VSCode.
 
   The following initial settings are provided for a fresh installation:
-""" + init_settings,
-        "C" -> (_ => check = true),
-        "f" -> (_ => fresh = true),
-        "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)),
-        "q" -> (_ => quiet = true))
+""" + init_settings)
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
-      val progress = new Console_Progress()
-      for (platform <- platforms) {
-        vscode_setup(check = check, platform = platform, quiet = quiet, fresh = fresh, progress = progress)
-      }
+      vscode_setup()
     })
 }