# HG changeset patch # User Thomas Lindae # Date 1718220121 -7200 # Node ID 4fa6e5f9d3939d98679f69392228ce59ed3d8c89 # Parent 2d3a0728cf1cc3884992fcf1bae2f98df5a2e0be lsp: extracted panel content generation logic; diff -r 2d3a0728cf1c -r 4fa6e5f9d393 src/Tools/VSCode/src/dynamic_output.scala --- a/src/Tools/VSCode/src/dynamic_output.scala Wed Jun 12 20:54:11 2024 +0200 +++ b/src/Tools/VSCode/src/dynamic_output.scala Wed Jun 12 21:22:01 2024 +0200 @@ -16,7 +16,6 @@ resources: VSCode_Resources, channel: Channel, restriction: Option[Set[Command]], - html_output: Boolean, margin: Double, force: Boolean, ): State = { @@ -39,26 +38,8 @@ else this } if (st1.output != output || force) { - 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 { - val (output, decorations) = resources.output_pretty_with_decorations(st1.output, margin) - channel.write(LSP.Dynamic_Output(output, Some(decorations))) - } + val (output, decorations) = resources.output_pretty_panel(st1.output, margin) + channel.write(LSP.Dynamic_Output(output, decorations)) } st1 } @@ -78,9 +59,8 @@ } private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = { - val html_output = server.resources.html_output state.change( - _.handle_update(server.resources, server.channel, restriction, html_output, margin, force)) + _.handle_update(server.resources, server.channel, restriction, margin, force)) } diff -r 2d3a0728cf1c -r 4fa6e5f9d393 src/Tools/VSCode/src/lsp.scala --- a/src/Tools/VSCode/src/lsp.scala Wed Jun 12 20:54:11 2024 +0200 +++ b/src/Tools/VSCode/src/lsp.scala Wed Jun 12 21:22:01 2024 +0200 @@ -478,7 +478,9 @@ JSON.optional("hover_message" -> MarkedStrings.json(hover_message)) } - sealed case class Decoration(decorations: List[(String, List[Decoration_Options])]) { + type Decoration_List = List[(String, List[Decoration_Options])] + + sealed case class Decoration(decorations: Decoration_List) { def json(file: JFile): JSON.T = Notification("PIDE/decoration", JSON.Object( @@ -532,7 +534,7 @@ /* dynamic output */ object Dynamic_Output { - def apply(content: String, decorations: Option[List[(String, List[Decoration_Options])]] = None): JSON.T = + def apply(content: String, decorations: Option[Decoration_List] = None): JSON.T = Notification("PIDE/dynamic_output", JSON.Object("content" -> content) ++ JSON.optional( @@ -561,7 +563,7 @@ id: Counter.ID, content: String, auto_update: Boolean, - decorations: Option[List[(String, List[Decoration_Options])]] = None + decorations: Option[Decoration_List] = None ): JSON.T = Notification("PIDE/state_output", JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update) ++ diff -r 2d3a0728cf1c -r 4fa6e5f9d393 src/Tools/VSCode/src/state_panel.scala --- a/src/Tools/VSCode/src/state_panel.scala Wed Jun 12 20:54:11 2024 +0200 +++ b/src/Tools/VSCode/src/state_panel.scala Wed Jun 12 21:22:01 2024 +0200 @@ -59,9 +59,7 @@ server.editor.send_dispatcher(update(force = true)) } - private def output( - content: String, - decorations: Option[List[(String, List[LSP.Decoration_Options])]] = None): Unit = + private def output(content: String, decorations: Option[LSP.Decoration_List] = None): Unit = server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value, decorations)) private def init_response(id: LSP.Id): Unit = @@ -76,26 +74,8 @@ new Query_Operation(server.editor, (), "print_state", _ => (), (_, _, body) => if (output_active.value && body.nonEmpty) { - 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.value) - val html = node_context.make_html(elements, formatted) - output(HTML.source(html).toString) - } else { - val (result, decorations) = server.resources.output_pretty_with_decorations(body, margin.value) - output(result, Some(decorations)) - } + val (result, decorations) = server.resources.output_pretty_panel(body, margin.value) + output(result, decorations) }) def locate(): Unit = print_state.locate_query() diff -r 2d3a0728cf1c -r 4fa6e5f9d393 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Wed Jun 12 20:54:11 2024 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jun 12 21:22:01 2024 +0200 @@ -343,35 +343,47 @@ 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) - def output_pretty_with_decorations( - body: XML.Body, - margin: Double, - ): (String, List[(String, List[LSP.Decoration_Options])]) = { - val separate = Pretty.separate(body) - val formatted = Pretty.formatted(separate, margin = margin) - - def convert_symbols(body: XML.Body): XML.Body = { - body.map { - case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body)) - case XML.Text(content) => XML.Text(Symbol.output(unicode_symbols, content)) - } - } + def output_pretty_panel(body: XML.Body, margin: Double): (String, Option[LSP.Decoration_List]) = { + val formatted = Pretty.formatted(Pretty.separate(body), margin = margin, metric = Symbol.Metric) - val tree = Markup_Tree.from_XML(convert_symbols(formatted)) - val output = output_pretty(separate, margin = margin) + 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 html = node_context.make_html(elements, formatted) + (HTML.source(html).toString, None) + } else { + def convert_symbols(body: XML.Body): XML.Body = { + body.map { + case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body)) + case XML.Text(content) => XML.Text(Symbol.output(unicode_symbols, content)) + } + } - val document = Line.Document(output) - val decorations = tree - .cumulate(Text.Range.full, None: Option[String], Rendering.text_color_elements, (_, m) => { - Some(Some(m.info.name)) - }) - .flatMap(e => e._2 match { - case None => None - case Some(i) => Some((document.range(e._1), "text_" ++ Rendering.text_color(i).toString)) - }) - .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList + val tree = Markup_Tree.from_XML(convert_symbols(formatted)) + val output = output_text(XML.content(formatted)) - (output, decorations) + val document = Line.Document(output) + val decorations = tree + .cumulate(Text.Range.full, None: Option[String], Rendering.text_color_elements, (_, m) => { + Some(Some(m.info.name)) + }) + .flatMap(e => e._2 match { + case None => None + case Some(i) => Some((document.range(e._1), "text_" ++ Rendering.text_color(i).toString)) + }) + .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList + + (output, Some(decorations)) + } }