provide vscode_extension via component, thus users don't need Node.js development tools;
proper default for edit_extension;
tuned messages;

--- a/Admin/components/components.sha1	Thu Mar 24 20:45:14 2022 +0100
+++ b/Admin/components/components.sha1	Thu Mar 24 22:27:17 2022 +0100
@@ -446,6 +446,7 @@
 c11d1120fcefaec79f099fe2be05b03cd2aed8b9  verit-2021.06-rmx.tar.gz
 b576fd5d89767c1067541d4839fb749c6a68d22c  verit-2021.06.1-rmx.tar.gz
 19c6e5677b0a26cbc5805da79d00d06a66b7a671  verit-2021.06.2-rmx.tar.gz
+c4666a6d8080b5e376b50471fd2d9edeb1f9c988  vscode_extension-20220324.tar.gz
 81d21dfd0ea5c58f375301f5166be9dbf8921a7a  windows_app-20130716.tar.gz
 fe15e1079cf5ad86f3cbab4553722a0d20002d11  windows_app-20130905.tar.gz
 e6a43b7b3b21295853bd2a63b27ea20bd6102f5f  windows_app-20130906.tar.gz

--- a/Admin/components/main	Thu Mar 24 20:45:14 2022 +0100
+++ b/Admin/components/main	Thu Mar 24 22:27:17 2022 +0100
@@ -29,6 +29,7 @@
 stack-2.7.3
 vampire-4.6
 verit-2021.06.2-rmx
+vscode_extension-20220324
 xz-java-1.9
 z3-4.4.0_4.4.1
 zipperposition-2.1-1

--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Thu Mar 24 20:45:14 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Thu Mar 24 22:27:17 2022 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Tools/VSCode/src/build_vscode_extension.scala
     Author:     Makarius
 
-Build the Isabelle/VSCode extension.
+Build the Isabelle/VSCode extension as component.
 */
 
 package isabelle.vscode
@@ -138,28 +138,63 @@
   /* build extension */
 
   def build_extension(options: Options,
+    target_dir: Path = Path.current,
     logic: String = default_logic,
     dirs: List[Path] = Nil,
-    progress: Progress = new Progress): File.Content =
+    progress: Progress = new Progress): Unit =
   {
     Isabelle_System.require_command("node")
     Isabelle_System.require_command("yarn")
     Isabelle_System.require_command("vsce")
 
-    Isabelle_System.with_tmp_dir("build")(build_dir =>
-    {
-      VSCode_Main.extension_manifest().prepare_dir(build_dir)
+
+    /* component */
+
+    val component_name = "vscode_extension-" + Date.Format.alt_date(Date.now())
+    val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
+    progress.echo("Component " + component_dir)
+
+
+    /* build */
 
-      build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)
+    val vsix_name =
+      Isabelle_System.with_tmp_dir("build")(build_dir =>
+      {
+        VSCode_Main.extension_manifest().prepare_dir(build_dir)
+
+        build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)
+
+        val result =
+          progress.bash("yarn && vsce package", cwd = build_dir.file, echo = true).check
+        val Pattern = """.*Packaged:.*(isabelle-.*\.vsix).*""".r
+        val vsix_name =
+          result.out_lines.collectFirst({ case Pattern(name) => name })
+            .getOrElse(error("Failed to guess resulting .vsix file name"))
 
-      val result =
-        progress.bash("yarn && vsce package", cwd = build_dir.file, echo = true).check
-      val Pattern = """.*Packaged:.*(isabelle-.*\.vsix).*""".r
-      val path =
-        result.out_lines.collectFirst({ case Pattern(name) => Path.explode(name) })
-          .getOrElse(error("Failed to guess resulting .vsix file name"))
-      File.Content(path, Bytes.read(build_dir + path))
-    })
+        Isabelle_System.copy_file(build_dir + Path.basic(vsix_name), component_dir)
+        vsix_name
+      })
+
+
+    /* settings */
+
+    val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+    File.write(etc_dir + Path.basic("settings"),
+      """# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_VSCODE_VSIX="$COMPONENT/""" + vsix_name + "\"\n")
+
+
+    /* README */
+
+    File.write(component_dir + Path.basic("README"),
+      """This the Isabelle/VSCode extension as VSIX package
+
+It has been produced from the sources in $ISABELLE_HOME/src/Tools/extension/.
+
+
+        Makarius
+        """ + Date.Format.date(Date.now()) + "\n")
   }
 
 
@@ -169,21 +204,22 @@
     Isabelle_Tool("build_vscode_extension", "build Isabelle/VSCode extension module",
       Scala_Project.here, args =>
     {
+      var target_dir = Path.current
       var dirs: List[Path] = Nil
       var logic = default_logic
-      var install = false
 
       val getopts = Getopts("""
 Usage: isabelle build_vscode_extension
 
   Options are:
-    -I           install resulting extension
+    -D DIR       target directory (default ".")
     -d DIR       include session directory
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
 
-Build Isabelle/VSCode extension module (vsix).
+Build the Isabelle/VSCode extension as component, for inclusion into the
+local VSCodium configuration.
 """,
-        "I" -> (_ => install = true),
+        "D:" -> (arg => target_dir = Path.explode(arg)),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "l:" -> (arg => logic = arg))
 
@@ -193,8 +229,7 @@
       val options = Options.init()
       val progress = new Console_Progress()
 
-      val vsix = build_extension(options, logic = logic, dirs = dirs, progress = progress)
-      vsix.write(VSCode_Main.extension_dir)
-      if (install) VSCode_Main.install_extension(vsix, progress = progress)
+      build_extension(options, target_dir = target_dir, logic = logic, dirs = dirs,
+        progress = progress)
     })
 }

--- a/src/Tools/VSCode/src/vscode_main.scala	Thu Mar 24 20:45:14 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Thu Mar 24 22:27:17 2022 +0100
@@ -75,13 +75,40 @@
 
   /* extension */
 
+  def default_vsix_path: Path = Path.explode("$ISABELLE_VSCODE_VSIX")
+
   def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension")
   def extension_manifest(): Manifest = new Manifest
   val extension_name: String = "isabelle.isabelle"
 
+  private val MANIFEST: Path = Path.explode("MANIFEST")
+
+  private def shasum_vsix(vsix_path: Path): String =
+  {
+    val name = "extension/MANIFEST.shasum"
+    def err(): Nothing = error("Cannot retrieve " + quote(name) + " from " + vsix_path)
+    if (vsix_path.is_file) {
+      using(new ZipFile(vsix_path.file))(zip_file =>
+      {
+        val entry = zip_file.getEntry(name)
+        if (entry == null) err()
+        else {
+          val stream = zip_file.getInputStream(entry)
+          if (stream == null) err() else File.read_stream(stream)
+        }
+      })
+    }
+    else err()
+  }
+
+  private def shasum_dir(dir: Path): Option[String] =
+  {
+    val path = dir + MANIFEST.shasum
+    if (path.is_file) Some(File.read(path)) else None
+  }
+
   final class Manifest private[VSCode_Main]
   {
-    private val MANIFEST: Path = Path.explode("MANIFEST")
     private val text = File.read(extension_dir + MANIFEST)
     private def entries: List[String] = split_lines(text).filter(_.nonEmpty)
 
@@ -94,26 +121,6 @@
       terminate_lines(a :: bs)
     }
 
-    def check_vsix(path: Path): Boolean =
-    {
-      path.is_file && {
-        using(new ZipFile(path.file))(zip_file =>
-        {
-          val entry = zip_file.getEntry("extension/MANIFEST.shasum")
-          entry != null && {
-            val stream = zip_file.getInputStream(entry)
-            stream != null && File.read_stream(stream) == extension_manifest().shasum
-          }
-        })
-      }
-    }
-
-    def check_dir(dir: Path): Boolean =
-    {
-      val path = dir + MANIFEST.shasum
-      path.is_file && File.read(path) == shasum
-    }
-
     def prepare_dir(dir: Path): Unit =
     {
       for (entry <- entries) {
@@ -136,21 +143,32 @@
       case None => progress.echo_warning("No Isabelle/VSCode extension to uninstall")
       case Some(dir) =>
         run_vscodium(List("--uninstall-extension", extension_name)).check
-        progress.echo("Uninstalled Isabelle/VSCode extension from directory:\n  " + dir)
+        progress.echo("Uninstalled Isabelle/VSCode extension from directory:\n" + dir)
     }
 
-  def install_extension(vsix: File.Content, progress: Progress = new Progress): Unit =
+  def install_extension(
+    vsix_path: Path = default_vsix_path,
+    progress: Progress = new Progress): Unit =
   {
-    Isabelle_System.with_tmp_dir("tmp")(tmp_dir =>
-    {
-      vsix.write(tmp_dir)
-      run_vscodium(List("--install-extension", File.platform_path(tmp_dir + vsix.path))).check
+    val new_shasum = shasum_vsix(vsix_path)
+    val old_shasum = locate_extension().flatMap(shasum_dir)
+    val current = old_shasum.isDefined && old_shasum.get == new_shasum
+
+    if (!current) {
+      run_vscodium(List("--install-extension", File.bash_platform_path(vsix_path))).check
       locate_extension() match {
-        case None => error("Missing extension Isabelle/VSCode after installation")
+        case None => error("Missing Isabelle/VSCode extension after installation")
         case Some(dir) =>
-          progress.echo("Installed Isabelle/VSCode extension into directory:\n  " + dir)
+          progress.echo("Installed Isabelle/VSCode extension " + vsix_path.expand +
+            "\ninto directory: " + dir)
       }
-    })
+      val manifest = extension_manifest()
+      if (manifest.shasum != new_shasum) {
+        progress.echo_warning(
+          "Isabelle/VSCode extension " + vsix_path.expand +
+            "\ndisagrees with project sources" + extension_dir.expand)
+      }
+    }
   }
 
 
@@ -189,10 +207,11 @@
     {
       var logic_ancestor = ""
       var console = false
-      var edit_extension = true
+      var edit_extension = false
       var server_log = false
       var logic_requirements = false
       var uninstall = false
+      var vsix_path = default_vsix_path
       var session_dirs = List.empty[Path]
       var include_sessions = List.empty[String]
       var logic = ""
@@ -213,6 +232,8 @@
                  """ + server_log_path.implode + """
     -R NAME      build image with requirements from other sessions
     -U           uninstall Isabelle/VSCode extension
+    -V FILE      specify VSIX file for Isabelle/VSCode extension
+                 (default: """ + default_vsix_path + """)
     -d DIR       include session directory
     -i NAME      include session in name-space of theories
     -l NAME      logic session name
@@ -235,6 +256,7 @@
         "L" -> (_ => server_log = true),
         "R:" -> (arg => { logic = arg; logic_requirements = true }),
         "U" -> (_ => uninstall = true),
+        "V" -> (arg => vsix_path = Path.explode(arg)),
         "d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))),
         "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
         "l:" -> (arg => { logic = arg; logic_requirements = false }),
@@ -253,6 +275,7 @@
       val console_progress = new Console_Progress
 
       if (uninstall) uninstall_extension(progress = console_progress)
+      else install_extension(vsix_path = vsix_path, progress = console_progress)
 
       val (background, app_progress) =
         if (console) (false, console_progress)