# HG changeset patch # User wenzelm # Date 1647859211 -3600 # Node ID c9ee3028c125f321ce7aa713f12bc81cc42111fd # Parent 9c72957e5c4a51950e6c3bc9ea1dd1dbbbed42e5 clean build from explicit MANIFEST: avoid accidental garbage in vsix package; diff -r 9c72957e5c4a -r c9ee3028c125 src/Tools/VSCode/extension/MANIFEST --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/MANIFEST Mon Mar 21 11:40:11 2022 +0100 @@ -0,0 +1,39 @@ +isabelle-language.json +isabelle-ml-grammar.json +isabelle-ml-language.json +isabelle.png +isabelle_vscode.png +media/main.js +media/Preview_inverse.svg +media/PreviewOnRightPane_16x_dark.svg +media/PreviewOnRightPane_16x.svg +media/Preview.svg +media/ViewSource_inverse.svg +media/ViewSource.svg +media/vscode.css +package.json +README.md +src/abbreviations.ts +src/completion.ts +src/decorations.ts +src/extension.ts +src/file.ts +src/library.ts +src/lsp.ts +src/output_view.ts +src/platform.ts +src/prefix_tree.ts +src/preview_panel.ts +src/script_decorations.ts +src/state_panel.ts +src/symbol.ts +src/vscode_lib.ts +test/extension.test.ts +test/index.ts +tsconfig.json +.vscodeignore +.vscode/launch.json +.vscode/settings.json +.vscode/tasks.json +yarn.lock +.yarnrc diff -r 9c72957e5c4a -r c9ee3028c125 src/Tools/VSCode/src/build_vscode_extension.scala --- a/src/Tools/VSCode/src/build_vscode_extension.scala Mon Mar 21 10:56:29 2022 +0100 +++ b/src/Tools/VSCode/src/build_vscode_extension.scala Mon Mar 21 11:40:11 2022 +0100 @@ -12,14 +12,11 @@ object Build_VSCode { - val extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension") - - /* build grammar */ def default_logic: String = Isabelle_System.getenv("ISABELLE_LOGIC") - def build_grammar(options: Options, + def build_grammar(options: Options, build_dir: Path, logic: String = default_logic, dirs: List[Path] = Nil, progress: Progress = new Progress): Unit = @@ -27,7 +24,7 @@ val keywords = Sessions.base_info(options, logic, dirs = dirs).check.base.overall_syntax.keywords - val output_path = extension_dir + Path.explode("isabelle-grammar.json") + val output_path = build_dir + Path.explode("isabelle-grammar.json") progress.echo(output_path.expand.implode) val (minor_keywords, operators) = @@ -140,31 +137,51 @@ /* extension */ + lazy val extension_dir = Path.explode("$ISABELLE_VSCODE_HOME/extension") + def uninstall_extension(progress: Progress = new Progress): Unit = progress.bash("isabelle vscode --uninstall-extension Isabelle.isabelle").check - def install_extension(vsix_path: Path, progress: Progress = new Progress): Unit = - progress.bash("isabelle vscode --install-extension " + - File.bash_platform_path(vsix_path)).check + def install_extension(vsix: File.Content, progress: Progress = new Progress): Unit = + { + Isabelle_System.with_tmp_dir("tmp")(tmp_dir => + { + vsix.write(tmp_dir) + progress.bash("isabelle vscode --install-extension " + + File.bash_platform_path(tmp_dir + vsix.path)).check + }) + } - def build_extension(progress: Progress = new Progress): Path = + def build_extension(options: Options, + logic: String = default_logic, + dirs: List[Path] = Nil, + progress: Progress = new Progress): File.Content = { Isabelle_System.require_command("node") Isabelle_System.require_command("yarn") Isabelle_System.require_command("vsce") - val output_path = extension_dir + Path.explode("out") - Isabelle_System.rm_tree(output_path) - Isabelle_System.make_directory(output_path) - progress.echo(output_path.expand.implode) + Isabelle_System.with_tmp_dir("build")(build_dir => + { + for { + line <- split_lines(File.read(extension_dir + Path.explode("MANIFEST"))) + if line.nonEmpty + } { + val path = Path.explode(line) + Isabelle_System.copy_file(extension_dir + path, + Isabelle_System.make_directory(build_dir + path.dir)) + } - val result = - progress.bash("yarn && vsce package", cwd = extension_dir.file, echo = true).check + build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress) - val Pattern = """.*Packaged:.*(isabelle-.*\.vsix).*""".r - result.out_lines.collectFirst( - { case Pattern(vsix_name) => extension_dir + Path.basic(vsix_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)) + }) } @@ -185,15 +202,15 @@ Options are: -I install resulting extension -U uninstall extension (no build) + -d DIR include session directory -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) -Build Isabelle/VSCode extension module in directory -""" + extension_dir.expand + """ +Build Isabelle/VSCode extension module (vsix). """, + "I" -> (_ => install = true), + "U" -> (_ => uninstall = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), - "l:" -> (arg => logic = arg), - "I" -> (_ => install = true), - "U" -> (_ => uninstall = true)) + "l:" -> (arg => logic = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() @@ -201,13 +218,11 @@ val options = Options.init() val progress = new Console_Progress() - if (uninstall) { - uninstall_extension(progress = progress) - } + if (uninstall) uninstall_extension(progress = progress) else { - build_grammar(options, logic = logic, dirs = dirs, progress = progress) - val path = build_extension(progress = progress) - if (install) install_extension(path, progress = progress) + val vsix = build_extension(options, logic = logic, dirs = dirs, progress = progress) + vsix.write(extension_dir) + if (install) install_extension(vsix, progress = progress) } }) }