add comments to rendering, e.g. to collect them from build database;

--- a/src/Pure/PIDE/rendering.scala	Thu Sep 26 14:44:37 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Fri Aug 23 15:30:09 2024 +0200
@@ -237,6 +237,10 @@
   val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
   val error_elements = Markup.Elements(Markup.ERROR)
 
+  val comment_elements =
+    Markup.Elements(Markup.ML_COMMENT, Markup.COMMENT, Markup.COMMENT1, Markup.COMMENT2,
+      Markup.COMMENT3)
+
   val entity_elements = Markup.Elements(Markup.ENTITY)
 
   val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
@@ -710,6 +714,12 @@
     snapshot.select(range, Rendering.error_elements, _ => Some(_)).map(_.info)
 
 
+  /* comments */
+
+  def comments(range: Text.Range): List[Text.Markup] =
+    snapshot.select(range, Rendering.comment_elements, _ => Some(_)).map(_.info)
+
+
   /* command status overview */
 
   def overview_color(range: Text.Range): Option[Rendering.Color.Value] = {