# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1720208439 -7200
# Node ID c87d2fa560ddf49f601da9794acea84aa1980bbf
# Parent  2ab384664ac571f64e6be8382b0685961f2b8264
vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors;

diff -r 2ab384664ac5 -r c87d2fa560dd src/Tools/VSCode/extension/package.json
--- 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",
diff -r 2ab384664ac5 -r c87d2fa560dd src/Tools/VSCode/src/component_vscode_extension.scala
--- 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)