clarified: add operation;
authorFabian Huch <huch@in.tum.de>
Wed, 02 Oct 2024 10:51:11 +0200
changeset 81085 fe69241e8786
parent 81084 96eb20106a34
child 81086 9c2628a73a3a
clarified: add operation;
src/Pure/System/options.scala
src/Tools/VSCode/src/component_vscode_extension.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
   }
--- 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 => (