# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1714559453 -7200
# Node ID d1535ba3b1ca6e5a8abc2439b749d2d56287f5f8
# Parent  8602af6f4bd0da838ec621c461913819847ddd60
lsp: added vscode_html_output option;

diff -r 8602af6f4bd0 -r d1535ba3b1ca src/Tools/VSCode/etc/options
--- 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"
diff -r 8602af6f4bd0 -r d1535ba3b1ca src/Tools/VSCode/extension/src/extension.ts
--- 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")
diff -r 8602af6f4bd0 -r d1535ba3b1ca src/Tools/VSCode/src/vscode_resources.scala
--- 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")