vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors;
--- a/src/Tools/VSCode/extension/package.json Fri Jul 05 13:30:07 2024 +0200
+++ b/src/Tools/VSCode/extension/package.json Fri Jul 05 21:40:39 2024 +0200
@@ -193,7 +193,7 @@
"configuration": {
"title": "Isabelle",
"properties": {
- /*options*/
+ "ISABELLE_OPTIONS": {},
"isabelle.replacement": {
"type": "string",
"default": "non-alphanumeric",
--- a/src/Tools/VSCode/src/component_vscode_extension.scala Fri Jul 05 13:30:07 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala Fri Jul 05 21:40:39 2024 +0200
@@ -231,7 +231,7 @@
val opt_json = options_json(options)
val package_path = build_dir + Path.basic("package.json")
- val package_body = File.read(package_path).replace("/*options*/", opt_json)
+ val package_body = File.read(package_path).replace("\"ISABELLE_OPTIONS\": {},", opt_json)
File.write(package_path, package_body)