# HG changeset patch
# User wenzelm
# Date 1733584068 -3600
# Node ID a7879978d15dacb3cda9852d3e872d18c2495d8a
# Parent  6dd6a6fa718b2505010632570ca15178f33baed0
tuned;

diff -r 6dd6a6fa718b -r a7879978d15d src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 16:03:05 2024 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 16:07:48 2024 +0100
@@ -74,11 +74,10 @@
       val text = XML.content(converted)
 
       val document = Line.Document(text)
-      val decorations = tree
-        .cumulate(Text.Range.full, None: Option[String], Rendering.text_color_elements, (_, m) => {
-          Some(Some(m.info.name))
-        })
-        .flatMap(e => e.info match {
+      val decorations =
+        tree.cumulate[Option[String]](Text.Range.full, None, Rendering.text_color_elements,
+          { case (_, m) => Some(Some(m.info.name)) }
+        ).flatMap(e => e.info match {
           case None => None
           case Some(i) => Some((document.range(e._1), "text_" ++ Rendering.text_color(i).toString))
         })