# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1718217850 -7200
# Node ID 45ef41e823f7065a800df44757cc90d30c310cc1
# Parent  fdc1281430ebef1580d6eb90ad1a12efbef40050
added vscode options tag;

diff -r fdc1281430eb -r 45ef41e823f7 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Thu May 30 02:43:29 2024 +0200
+++ b/src/Pure/System/options.scala	Wed Jun 12 20:44:10 2024 +0200
@@ -109,6 +109,7 @@
   val TAG_UPDATE = "update"      // relevant for "isabelle update"
   val TAG_CONNECTION = "connection"  // private information about connections (password etc.)
   val TAG_COLOR_DIALOG = "color_dialog"  // special color selection dialog
+  val TAG_VSCODE = "vscode"      // relevant for "isabelle vscode" and "isabelle vscode_server"
 
   case class Entry(
     public: Boolean,
diff -r fdc1281430eb -r 45ef41e823f7 src/Tools/VSCode/etc/options
--- a/src/Tools/VSCode/etc/options	Thu May 30 02:43:29 2024 +0200
+++ b/src/Tools/VSCode/etc/options	Wed Jun 12 20:44:10 2024 +0200
@@ -1,34 +1,34 @@
 (* :mode=isabelle-options: *)
 
-option vscode_input_delay : real = 0.1
+option vscode_input_delay : real = 0.1 for vscode
   -- "delay for client input (edits)"
 
-option vscode_output_delay : real = 0.5
+option vscode_output_delay : real = 0.5 for vscode
   -- "delay for client output (rendering)"
 
-option vscode_load_delay : real = 0.5
+option vscode_load_delay : real = 0.5 for vscode
   -- "delay for file load operations"
 
-option vscode_tooltip_margin : int = 60
+option vscode_tooltip_margin : int = 60 for vscode
   -- "margin for pretty-printing of tooltips"
 
-option vscode_message_margin : int = 80
+option vscode_message_margin : int = 80 for vscode
   -- "margin for pretty-printing of diagnostic messages"
 
-option vscode_timing_threshold : real = 0.1
+option vscode_timing_threshold : real = 0.1 for vscode
   -- "default threshold for timing display (seconds)"
 
-option vscode_pide_extensions : bool = false
+option vscode_pide_extensions : bool = false for vscode
   -- "use PIDE extensions for Language Server Protocol"
 
-option vscode_unicode_symbols : bool = false
+option vscode_unicode_symbols : bool = false for vscode
   -- "output Isabelle symbols via Unicode (according to etc/symbols)"
 
-option vscode_caret_perspective : int = 50
+option vscode_caret_perspective : int = 50 for vscode
   -- "number of visible lines above and below the caret (0: unrestricted)"
 
-option vscode_caret_preview : bool = false
+option vscode_caret_preview : bool = false for vscode
   -- "dynamic preview of caret document node"
 
-option vscode_html_output : bool = false
+option vscode_html_output : bool = false for vscode
   -- "output State and Output in HTML"