# HG changeset patch # User Fabian Huch # 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 => (