--- 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")