src/Tools/VSCode/src/pretty_text_panel.scala

--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Jun 30 15:32:45 2024 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sun Jun 30 15:32:51 2024 +0200
@@ -75,7 +75,7 @@
         .cumulate(Text.Range.full, None: Option[String], Rendering.text_color_elements, (_, m) => {
           Some(Some(m.info.name))
         })
-        .flatMap(e => e._2 match {
+        .flatMap(e => e.info match {
           case None => None
           case Some(i) => Some((document.range(e._1), "text_" ++ Rendering.text_color(i).toString))
         })