# HG changeset patch # User wenzelm # Date 1648039393 -3600 # Node ID d07c886a27a9efa662e4e7e36f08c212f5c000ff # Parent e641ac92b489e868d72fd23a736020d8de390cd5 more robust install/uninstall; clarified extension_name (again): --locate-extension wants to see a lowercase name; diff -r e641ac92b489 -r d07c886a27a9 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Wed Mar 23 13:05:54 2022 +0100 +++ b/src/Tools/VSCode/extension/package.json Wed Mar 23 13:43:13 2022 +0100 @@ -11,7 +11,7 @@ ], "icon": "isabelle.png", "version": "2.0.0", - "publisher": "Isabelle", + "publisher": "isabelle", "license": "MIT", "repository": { "url": "https://isabelle-dev.sketis.net" diff -r e641ac92b489 -r d07c886a27a9 src/Tools/VSCode/src/vscode_main.scala --- a/src/Tools/VSCode/src/vscode_main.scala Wed Mar 23 13:05:54 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_main.scala Wed Mar 23 13:43:13 2022 +0100 @@ -75,6 +75,7 @@ def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension") def extension_manifest(): Manifest = new Manifest + val extension_name: String = "isabelle.isabelle" final class Manifest private[VSCode_Main] { @@ -108,16 +109,33 @@ } } + def locate_extension(): Option[Path] = + { + val out = run_vscodium(List("--locate-extension", extension_name)).check.out + if (out.nonEmpty) Some(Path.explode(File.standard_path(out))) else None + } + def uninstall_extension(progress: Progress = new Progress): Unit = - run_vscodium(List("--uninstall-extension", "Isabelle.isabelle"), progress = progress).check + locate_extension() match { + case None => progress.echo_warning("No extension " + quote(extension_name) + " to uninstall") + case Some(dir) => + run_vscodium(List("--uninstall-extension", extension_name)).check + progress.echo("Uninstalled extension " + quote(extension_name) + + " from directory:\n " + dir) + } def install_extension(vsix: File.Content, 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)), - progress = progress).check + run_vscodium(List("--install-extension", File.platform_path(tmp_dir + vsix.path))).check + locate_extension() match { + case None => error("No extension " + extension_name + " after installation") + case Some(dir) => + progress.echo("Installed extension " + quote(extension_name) + + " into directory:\n " + dir) + } }) }