vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors;
authorThomas Lindae <thomas.lindae@in.tum.de>
Fri, 05 Jul 2024 21:40:39 +0200
changeset 81074 c87d2fa560dd
parent 81073 2ab384664ac5
child 81075 f0341e6b1b30
vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors;
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/src/component_vscode_extension.scala
--- 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)