--- a/src/Tools/VSCode/src/dynamic_output.scala Wed May 01 12:30:53 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala Wed May 01 12:34:53 2024 +0200
@@ -15,7 +15,9 @@
def handle_update(
resources: VSCode_Resources,
channel: Channel,
- restriction: Option[Set[Command]]
+ restriction: Option[Set[Command]],
+ html_output: Boolean,
+ margin: Double,
): State = {
val st1 =
resources.get_caret() match {
@@ -36,19 +38,25 @@
else this
}
if (st1.output != output) {
- val node_context =
- new Browser_Info.Node_Context {
- override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
- for {
- thy_file <- Position.Def_File.unapply(props)
- def_line <- Position.Def_Line.unapply(props)
- source <- resources.source_file(thy_file)
- uri = File.uri(Path.explode(source).absolute_file)
- } yield HTML.link(uri.toString + "#" + def_line, body)
- }
- val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
- val html = node_context.make_html(elements, Pretty.separate(st1.output))
- channel.write(LSP.Dynamic_Output(HTML.source(html).toString))
+ if (html_output) {
+ val node_context =
+ new Browser_Info.Node_Context {
+ override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
+ for {
+ thy_file <- Position.Def_File.unapply(props)
+ def_line <- Position.Def_Line.unapply(props)
+ source <- resources.source_file(thy_file)
+ uri = File.uri(Path.explode(source).absolute_file)
+ } yield HTML.link(uri.toString + "#" + def_line, body)
+ }
+ val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
+ val separate = Pretty.separate(st1.output)
+ val formatted = Pretty.formatted(separate, margin = margin)
+ 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)))
+ }
}
st1
}
@@ -60,9 +68,12 @@
class Dynamic_Output private(server: Language_Server) {
private val state = Synchronized(Dynamic_Output.State())
+ private val margin: Double = 80
- private def handle_update(restriction: Option[Set[Command]]): Unit =
- state.change(_.handle_update(server.resources, server.channel, restriction))
+ private def handle_update(restriction: Option[Set[Command]]): Unit = {
+ val html_output = server.resources.html_output
+ state.change(_.handle_update(server.resources, server.channel, restriction, html_output, margin))
+ }
/* main */
--- a/src/Tools/VSCode/src/state_panel.scala Wed May 01 12:30:53 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Wed May 01 12:34:53 2024 +0200
@@ -47,6 +47,7 @@
/* output */
val id: Counter.ID = State_Panel.make_id()
+ private val margin: Double = 80
private def output(content: String): Unit =
server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value))
@@ -63,19 +64,25 @@
new Query_Operation(server.editor, (), "print_state", _ => (),
(_, _, body) =>
if (output_active.value && body.nonEmpty) {
- val node_context =
- new Browser_Info.Node_Context {
- override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
- for {
- thy_file <- Position.Def_File.unapply(props)
- def_line <- Position.Def_Line.unapply(props)
- source <- server.resources.source_file(thy_file)
- uri = File.uri(Path.explode(source).absolute_file)
- } yield HTML.link(uri.toString + "#" + def_line, body)
- }
- val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
- val html = node_context.make_html(elements, Pretty.separate(body))
- output(HTML.source(html).toString)
+ if (server.resources.html_output) {
+ val node_context =
+ new Browser_Info.Node_Context {
+ override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
+ for {
+ thy_file <- Position.Def_File.unapply(props)
+ def_line <- Position.Def_Line.unapply(props)
+ source <- server.resources.source_file(thy_file)
+ uri = File.uri(Path.explode(source).absolute_file)
+ } yield HTML.link(uri.toString + "#" + def_line, body)
+ }
+ val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
+ val separate = Pretty.separate(body)
+ val formatted = Pretty.formatted(separate, margin = margin)
+ val html = node_context.make_html(elements, formatted)
+ output(HTML.source(html).toString)
+ } else {
+ output(server.resources.output_pretty(body, margin))
+ }
})
def locate(): Unit = print_state.locate_query()
--- a/src/Tools/VSCode/src/vscode_resources.scala Wed May 01 12:30:53 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed May 01 12:34:53 2024 +0200
@@ -337,7 +337,7 @@
def output_xml(xml: XML.Tree): String =
output_text(XML.content(xml))
- def output_pretty(body: XML.Body, margin: Int): String =
+ def output_pretty(body: XML.Body, margin: Double): String =
output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric))
def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)