# HG changeset patch # User Fabian Huch <huch@in.tum.de> # Date 1724419809 -7200 # Node ID 97924a26a5c3e80da3f7c17f9bf13239dc558363 # Parent 572970d15ab06a2c7cf7a5038e8ddf6565221745 add comments to rendering, e.g. to collect them from build database; diff -r 572970d15ab0 -r 97924a26a5c3 src/Pure/PIDE/rendering.scala --- 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] = {