--- a/src/Tools/VSCode/src/pretty_text_panel.scala Sat Nov 01 14:22:26 2025 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala Sat Nov 01 14:32:12 2025 +0100
@@ -23,6 +23,8 @@
channel: Channel,
output_json: (String, Option[LSP.Decoration]) => JSON.T
) {
+ def resources: VSCode_Resources = session.resources
+
private var current_output: List[XML.Elem] = Nil
private var current_formatted: XML.Body = Nil
private var margin: Double = resources.message_margin
@@ -31,8 +33,6 @@
refresh(current_output)
}
- def resources: VSCode_Resources = session.resources
-
def update_margin(new_margin: Double): Unit = {
margin = new_margin
delay_margin.invoke()
@@ -66,7 +66,8 @@
val document = Line.Document(converted_text)
val decorations =
- converted_tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements,
+ converted_tree.cumulate[Option[Markup]](
+ Text.Range.full, None, Rendering.text_color_elements,
{ case (_, m) => Some(Some(m.info.markup)) }
).flatMap(info =>
info.info match {