src/Pure/PIDE/rendering.scala

--- a/src/Pure/PIDE/rendering.scala	Fri Nov 01 15:40:31 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Fri Nov 01 16:53:10 2024 +0100
@@ -222,6 +222,11 @@
 
   val text_color_elements = Markup.Elements(text_color.keySet)
 
+  val structure_elements =
+    Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
+      Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
+      Markup.COMMAND_SPAN)
+
   val tooltip_elements =
     Markup.Elements(Markup.LANGUAGE, Markup.NOTATION, Markup.EXPRESSION, Markup.TIMING,
       Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
@@ -572,6 +577,26 @@
   }
 
 
+  /* markup structure */
+
+  def markup_structure(
+    elements: Markup.Elements,
+    ranges: List[Text.Range],
+    filter: Text.Markup => Boolean = _ => true
+  ): List[Text.Markup] = {
+    def cumulate(range: Text.Range): List[Text.Info[Option[Text.Markup]]] =
+      snapshot.cumulate[Option[Text.Markup]](range, None, elements, _ =>
+        {
+          case (old, markup) =>
+            Some(if (old.isEmpty || filter(markup)) Some(markup) else old)
+        })
+
+    Library.distinct(
+      for (range <- ranges; case Text.Info(_, Some(m)) <- cumulate(range))
+        yield m)
+  }
+
+
   /* tooltips */
 
   def timing_threshold: Double = 0.0