# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1714760028 -7200
# Node ID c25fed2d0e78c43efd2b69a4533987241f810929
# Parent  de94fcfbc3cef45a72d441764d778a4162479224
lsp: added separation for non-html output and state;

diff -r de94fcfbc3ce -r c25fed2d0e78 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Fri May 03 20:11:41 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Fri May 03 20:13:48 2024 +0200
@@ -56,7 +56,8 @@
           val html = node_context.make_html(elements, formatted)
           channel.write(LSP.Dynamic_Output(HTML.source(html).toString))
         } else {
-          channel.write(LSP.Dynamic_Output(resources.output_pretty(st1.output, margin = margin)))
+          val output = resources.output_pretty(Pretty.separate(st1.output), margin = margin)
+          channel.write(LSP.Dynamic_Output(output))
         }
       }
       st1
diff -r de94fcfbc3ce -r c25fed2d0e78 src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Fri May 03 20:11:41 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Fri May 03 20:13:48 2024 +0200
@@ -87,7 +87,7 @@
             val html = node_context.make_html(elements, formatted)
             output(HTML.source(html).toString)
           } else {
-            output(server.resources.output_pretty(body, margin))
+            output(server.resources.output_pretty(Pretty.separate(body), margin))
           }
         })