# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1727859071 -7200
# Node ID fe69241e87867df2965cd055740849e9ac0e25d5
# Parent  96eb20106a34f6e273ff207a54f6da448971be58
clarified: add operation;

diff -r 96eb20106a34 -r fe69241e8786 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Oct 02 10:39:32 2024 +0200
+++ b/src/Pure/System/options.scala	Wed Oct 02 10:51:11 2024 +0200
@@ -157,6 +157,7 @@
     def for_document: Boolean = for_tag(TAG_DOCUMENT)
     def for_color_dialog: Boolean = for_tag(TAG_COLOR_DIALOG)
     def for_build_sync: Boolean = for_tag(TAG_BUILD_SYNC)
+    def for_vscode: Boolean = for_tag(TAG_VSCODE)
 
     def session_content: Boolean = for_content || for_document
   }
diff -r 96eb20106a34 -r fe69241e8786 src/Tools/VSCode/src/component_vscode_extension.scala
--- a/src/Tools/VSCode/src/component_vscode_extension.scala	Wed Oct 02 10:39:32 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala	Wed Oct 02 10:51:11 2024 +0200
@@ -150,7 +150,7 @@
 
     (for {
       opt <- options.iterator
-      if opt.for_tag(Options.TAG_VSCODE) || opt.for_content || relevant_options.contains(opt.name)
+      if opt.for_vscode || opt.for_content || relevant_options.contains(opt.name)
     } yield {
       val (enum_values, enum_descriptions) = opt.typ match {
         case Options.Bool => (