src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Sun Jun 29 15:53:45 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun Jun 29 16:16:22 2025 +0200
@@ -626,6 +626,14 @@
   val NO_REPORT = "no_report"
 
   val BAD = "bad"
+  object Bad {
+    def apply(serial: Long): Markup = Markup(BAD, Serial(serial))
+    def unapply(markup: Markup): Option[Long] =
+      markup match {
+        case Markup(BAD, Serial(i)) => Some(i)
+        case _ => None
+      }
+  }
 
   val INTENSIFY = "intensify"