src/Pure/PIDE/rendering.scala
changeset 71499 29f37eb9bd0f
parent 70135 ad6d4a14adb5
child 71555 7eadccd4392c
--- a/src/Pure/PIDE/rendering.scala	Sun Mar 01 15:20:47 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Mar 01 21:52:21 2020 +0100
@@ -208,6 +208,9 @@
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
       Markup.BAD)
 
+  val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
+  val error_elements = Markup.Elements(Markup.ERROR)
+
   val caret_focus_elements = Markup.Elements(Markup.ENTITY)
 
   val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
@@ -653,6 +656,15 @@
   }
 
 
+  /* messages */
+
+  def warnings(range: Text.Range): List[Text.Markup] =
+    snapshot.select(range, Rendering.warning_elements, _ => Some(_)).map(_.info)
+
+  def errors(range: Text.Range): List[Text.Markup] =
+    snapshot.select(range, Rendering.error_elements, _ => Some(_)).map(_.info)
+
+
   /* command status overview */
 
   def overview_color(range: Text.Range): Option[Rendering.Color.Value] =