# HG changeset patch
# User wenzelm
# Date 1733604545 -3600
# Node ID 871caa4b3142de034da52e7d65369219c814a10b
# Parent  4eba973e8a7be2004f318b4c548484e95a357b61
tuned;

diff -r 4eba973e8a7b -r 871caa4b3142 src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 21:42:59 2024 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 21:49:05 2024 +0100
@@ -77,12 +77,14 @@
       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(name) =>
-            Some((document.range(e._1), "text_" ++ Rendering.get_text_color(name).get.toString))
-        })
-        .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList
+        ).flatMap(info =>
+            info.info match {
+              case Some(name) =>
+                val range = document.range(info.range)
+                Some((range, "text_" + Rendering.get_text_color(name).get.toString))
+              case None => None
+            }
+        ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList
 
       channel.write(output_json(text, Some(LSP.Decoration(decorations))))
     }