lsp: added vscode_html_output option;
authorThomas Lindae <thomas.lindae@in.tum.de>
Wed, 01 May 2024 12:30:53 +0200
changeset 81024 d1535ba3b1ca
parent 81023 8602af6f4bd0
child 81025 d4eb94b46e83
lsp: added vscode_html_output option;
src/Tools/VSCode/etc/options
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/etc/options	Wed May 01 11:12:59 2024 +0200
+++ b/src/Tools/VSCode/etc/options	Wed May 01 12:30:53 2024 +0200
@@ -29,3 +29,6 @@
 
 option vscode_caret_preview : bool = false
   -- "dynamic preview of caret document node"
+
+option vscode_html_output : bool = false
+  -- "output State and Output in HTML"
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed May 01 11:12:59 2024 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed May 01 12:30:53 2024 +0200
@@ -65,6 +65,7 @@
 
   add("-o"); add("vscode_unicode_symbols")
   add("-o"); add("vscode_pide_extensions")
+  add("-o"); add("vscode_html_output")
   add_values("-o", "options")
 
   add_value("-A", "logic_ancestor")
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed May 01 11:12:59 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed May 01 12:30:53 2024 +0200
@@ -81,6 +81,7 @@
 
   def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
   def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
+  def html_output: Boolean = options.bool("vscode_html_output")
   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
   def message_margin: Int = options.int("vscode_message_margin")