--- a/Admin/components/components.sha1 Thu Mar 24 22:43:41 2022 +0000
+++ b/Admin/components/components.sha1 Thu Mar 24 23:54:40 2022 +0100
@@ -446,6 +446,8 @@
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
+67b271186631f84efd97246bf85f6d8cfaa5edfd vscodium-1.65.2.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 22:43:41 2022 +0000
+++ b/Admin/components/main Thu Mar 24 23:54:40 2022 +0100
@@ -29,6 +29,8 @@
stack-2.7.3
vampire-4.6
verit-2021.06.2-rmx
+vscode_extension-20220324
+vscodium-1.65.2
xz-java-1.9
z3-4.4.0_4.4.1
zipperposition-2.1-1
--- a/NEWS Thu Mar 24 22:43:41 2022 +0000
+++ b/NEWS Thu Mar 24 23:54:40 2022 +0100
@@ -15,9 +15,15 @@
*** Isabelle/VSCode Prover IDE ***
-* Command-line tools "isabelle vscode_setup" and "isabelle vscode"
-provide convenient access to a well-defined version of VSCodium
-(open-source distribution of VSCode without MS telemetry).
+* VSCodium, an open-source distribution of VSCode without MS
+telemetry, has been bundled with Isabelle as add-on component. The
+command-line tool "isabelle vscode" automatically configures it as
+Isabelle/VSCode and starts the application.
+
+* Command-line tools "isabelle electron" and "isabelle node" provide
+access to the underlying technologies of VSCodium, for use in other
+applications. This essentially provides a freely programmable Chromium
+browser engine that works uniformly on all platforms.
*** HOL ***
--- a/src/Tools/VSCode/src/build_vscode_extension.scala Thu Mar 24 22:43:41 2022 +0000
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala Thu Mar 24 23:54:40 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,24 +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
- var uninstall = false
val getopts = Getopts("""
Usage: isabelle build_vscode_extension
Options are:
- -I install resulting extension
- -U uninstall extension (no build)
+ -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),
- "U" -> (_ => uninstall = true),
+ "D:" -> (arg => target_dir = Path.explode(arg)),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"l:" -> (arg => logic = arg))
@@ -196,11 +229,7 @@
val options = Options.init()
val progress = new Console_Progress()
- if (uninstall) VSCode_Main.uninstall_extension(progress = progress)
- else {
- 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 22:43:41 2022 +0000
+++ b/src/Tools/VSCode/src/vscode_main.scala Thu Mar 24 23:54:40 2022 +0100
@@ -75,13 +75,16 @@
/* extension */
+ def default_vsix_path: Path = Path.explode("$ISABELLE_VSCODE_VSIX")
+
def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension")
+ val extension_name: String = "isabelle.isabelle"
def extension_manifest(): Manifest = new Manifest
- val extension_name: String = "isabelle.isabelle"
+
+ private val MANIFEST: Path = Path.explode("MANIFEST")
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 +97,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) {
@@ -125,6 +108,30 @@
}
}
+ 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 =>
+ zip_file.getEntry(name) match {
+ case null => err()
+ case entry =>
+ zip_file.getInputStream(entry) match {
+ case null => err()
+ case stream => 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
+ }
+
def locate_extension(): Option[Path] =
{
val out = run_vscodium(List("--locate-extension", extension_name)).check.out
@@ -133,26 +140,35 @@
def uninstall_extension(progress: Progress = new Progress): Unit =
locate_extension() match {
- case None => progress.echo_warning("No extension " + quote(extension_name) + " to uninstall")
+ 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 extension " + quote(extension_name) +
- " 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("No extension " + extension_name + " after installation")
+ case None => error("Missing Isabelle/VSCode extension after installation")
case Some(dir) =>
- progress.echo("Installed extension " + quote(extension_name) +
- " 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)
+ }
+ }
}
@@ -191,8 +207,11 @@
{
var logic_ancestor = ""
var console = false
+ 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 = ""
@@ -208,9 +227,13 @@
-A NAME ancestor session for option -R (default: parent)
-C run as foreground process, with console output
+ -E edit Isabelle/VSCode extension project sources
-L enable language server log to file:
""" + 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
@@ -229,8 +252,11 @@
""" + default_settings,
"A:" -> (arg => logic_ancestor = arg),
"C" -> (_ => console = true),
+ "E" -> (_ => edit_extension = true),
"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 }),
@@ -246,14 +272,21 @@
init_settings()
- val (background, progress) =
- if (console) (false, new Console_Progress)
+ 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)
else { run_vscodium(List("--version")).check; (true, new Progress) }
- run_vscodium(more_args, options = options, logic = logic, logic_ancestor = logic_ancestor,
+ run_vscodium(
+ more_args ::: (if (edit_extension) List(File.platform_path(extension_dir)) else Nil),
+ options = options, logic = logic, logic_ancestor = logic_ancestor,
logic_requirements = logic_requirements, session_dirs = session_dirs,
include_sessions = include_sessions, modes = modes, no_build = no_build,
server_log = server_log, verbose = verbose, background = background,
- progress = progress).check
+ progress = app_progress).check
})
}