# HG changeset patch # User Thomas Lindae # Date 1714559693 -7200 # Node ID d4eb94b46e83808b7c445afced3f1e91744593da # Parent d1535ba3b1ca6e5a8abc2439b749d2d56287f5f8 lsp: added State and Dynamic Output html_output and margin handling; diff -r d1535ba3b1ca -r d4eb94b46e83 src/Tools/VSCode/src/dynamic_output.scala --- 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 */ diff -r d1535ba3b1ca -r d4eb94b46e83 src/Tools/VSCode/src/state_panel.scala --- 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() diff -r d1535ba3b1ca -r d4eb94b46e83 src/Tools/VSCode/src/vscode_resources.scala --- 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)