--- a/src/Tools/VSCode/src/dynamic_output.scala Mon May 27 13:21:15 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala Thu May 30 02:43:24 2024 +0200
@@ -56,30 +56,7 @@
val html = node_context.make_html(elements, formatted)
channel.write(LSP.Dynamic_Output(HTML.source(html).toString))
} else {
- val separate = Pretty.separate(st1.output)
- 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(resources.unicode_symbols, content))
- }
- }
-
- val tree = Markup_Tree.from_XML(convert_symbols(formatted))
- val output = resources.output_pretty(separate, margin = margin)
-
- 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 (output, decorations) = resources.output_pretty_with_decorations(st1.output, margin)
channel.write(LSP.Dynamic_Output(output, Some(decorations)))
}
}
--- a/src/Tools/VSCode/src/state_panel.scala Mon May 27 13:21:15 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Thu May 30 02:43:24 2024 +0200
@@ -93,30 +93,7 @@
val html = node_context.make_html(elements, formatted)
output(HTML.source(html).toString)
} else {
- val separate = Pretty.separate(body)
- val formatted = Pretty.formatted(separate, margin = margin.value)
-
- 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(server.resources.unicode_symbols, content))
- }
- }
-
- val tree = Markup_Tree.from_XML(convert_symbols(formatted))
- val result = server.resources.output_pretty(separate, margin = margin.value)
-
- val document = Line.Document(result)
- 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 (result, decorations) = server.resources.output_pretty_with_decorations(body, margin.value)
output(result, Some(decorations))
}
})
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon May 27 13:21:15 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Thu May 30 02:43:24 2024 +0200
@@ -343,6 +343,37 @@
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))
+ }
+ }
+
+ val tree = Markup_Tree.from_XML(convert_symbols(formatted))
+ val output = output_pretty(separate, margin = margin)
+
+ 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, decorations)
+ }
+
/* caret handling */