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