--- 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] = {