lsp: added separation for non-html output and state;
authorThomas Lindae <thomas.lindae@in.tum.de>
Fri, 03 May 2024 20:13:48 +0200
changeset 81033 c25fed2d0e78
parent 81032 de94fcfbc3ce
child 81034 50082e028475
lsp: added separation for non-html output and state;
src/Tools/VSCode/src/dynamic_output.scala
src/Tools/VSCode/src/state_panel.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
--- 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))
           }
         })