# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1719754312 -7200
# Node ID 82c951b34559b90200e1fba2b5e6e3159aaec8a9
# Parent  ccbddf0372c4052ecd247ef1892cffadd9b1e7e5
vscode: added more relevant options;

diff -r ccbddf0372c4 -r 82c951b34559 src/Tools/VSCode/src/component_vscode_extension.scala
--- a/src/Tools/VSCode/src/component_vscode_extension.scala	Fri Jun 14 10:21:47 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala	Sun Jun 30 15:31:52 2024 +0200
@@ -135,7 +135,18 @@
   
 
   private def options_json(options: Options): String = {
-    val relevant_options = Set("editor_output_state")
+    val relevant_options = Set(
+      "editor_output_state",
+      "auto_time_start",
+      "auto_time_limit",
+      "auto_nitpick",
+      "auto_sledgehammer",
+      "auto_methods",
+      "auto_quickcheck",
+      "auto_solve_direct",
+      "sledgehammer_provers",
+      "sledgehammer_timeout",
+    )
     
     options.iterator.filter(
       opt => opt.for_tag(Options.TAG_VSCODE) || opt.for_content || relevant_options.contains(opt.name)