# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1718220391 -7200
# Node ID 9cedc1fbed0fe688123fce84fcc584049c2709aa
# Parent  42dafe6efb8d73e6211099cff8d80316ca73c514
vscode: added relevant isabelle options to vscode settings;

diff -r 42dafe6efb8d -r 9cedc1fbed0f src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Wed Jun 12 21:14:41 2024 +0200
+++ b/src/Tools/VSCode/extension/package.json	Wed Jun 12 21:26:31 2024 +0200
@@ -193,6 +193,7 @@
         "configuration": {
             "title": "Isabelle",
             "properties": {
+                /*options*/
                 "isabelle.replacement": {
                     "type": "string",
                     "default": "non-alphanumeric",
diff -r 42dafe6efb8d -r 9cedc1fbed0f src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Jun 12 21:14:41 2024 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Jun 12 21:26:31 2024 +0200
@@ -63,11 +63,6 @@
     }
   }
 
-  add("-o"); add("vscode_unicode_symbols")
-  add("-o"); add("vscode_pide_extensions")
-  add("-o"); add("vscode_html_output")
-  add_values("-o", "options")
-
   add_value("-A", "logic_ancestor")
   if (args.logic) { add_value(args.logic_requirements ? "-R" : "-l", "logic") }
 
@@ -77,6 +72,17 @@
   add_value("-L", "log_file")
   if (args.verbose) { add("-v") }
 
+  const config = workspace.getConfiguration("isabelle.options")
+  Object.keys(config).forEach(key =>
+  {
+    const value = config[key]
+    if (typeof value == "string" && value !== "")
+    {
+      add("-o"); add(`${key}=${value}`)
+    }
+  })
+  add_values("-o", "options")
+
   return result
 }
 
diff -r 42dafe6efb8d -r 9cedc1fbed0f src/Tools/VSCode/src/component_vscode_extension.scala
--- a/src/Tools/VSCode/src/component_vscode_extension.scala	Wed Jun 12 21:14:41 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala	Wed Jun 12 21:26:31 2024 +0200
@@ -132,6 +132,38 @@
 }
 """)
   }
+  
+
+  private def options_json(options: Options): String = {
+    val relevant_options = Set("editor_output_state")
+    
+    options.iterator.filter(
+      opt => opt.for_tag(Options.TAG_VSCODE) || opt.for_content || relevant_options.contains(opt.name)
+    ).map(opt => {
+      val (enum_values, enum_descriptions) = opt.typ match {
+        case Options.Bool => (
+          Some(List("", "true", "false")),
+          Some(List("Don't overwrite System Preference.", "Enable.", "Disable."))
+        )
+        case _ => (None, None)
+      }
+
+      val default = opt.name match {
+        case "vscode_unicode_symbols" => "true"
+        case "vscode_pide_extensions" => "true"
+        case "vscode_html_output" => "true"
+        case _ => ""
+      }
+
+      quote("isabelle.options." + opt.name) + ": " + JSON.Format(
+        JSON.Object(
+          "type" -> "string",
+          "default" -> default,
+          "description" -> opt.description,
+        ) ++ JSON.optional("enum" -> enum_values) ++ JSON.optional("enumDescriptions" -> enum_descriptions)
+      ) + ","
+    }).mkString
+  }
 
 
   /* build extension */
@@ -182,6 +214,15 @@
         }
         File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum.toString)
 
+
+        /* options */
+
+        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)
+        File.write(package_path, package_body)
+
+
         build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)
 
         val result =