# HG changeset patch
# User wenzelm
# Date 1751206582 -7200
# Node ID ad3860303ebbb73c273391cc5f343d0484a1d4bf
# Parent  0bc9dbc61f7f558a797215f21d2b066c8bfa9821
clarified signature: more explicit operations;

diff -r 0bc9dbc61f7f -r ad3860303ebb 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"
 
diff -r 0bc9dbc61f7f -r ad3860303ebb src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Jun 29 15:53:45 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Sun Jun 29 16:16:22 2025 +0200
@@ -454,7 +454,7 @@
               case ((markups, color), Text.Info(_, XML.Elem(markup, _)))
               if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) =>
                 Some((markup :: markups, color))
-              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
+              case (_, Text.Info(_, XML.Elem(Markup.Bad(_), _))) =>
                 Some((Nil, Some(Rendering.Color.bad)))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                 Some((Nil, Some(Rendering.Color.intensify)))
@@ -666,7 +666,7 @@
         {
           case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info.add_timing(t))
 
-          case (info, Text.Info(r0, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body)))
+          case (info, Text.Info(r0, msg @ XML.Elem(Markup.Bad(i), body)))
           if body.nonEmpty => Some(info.add_message(r0, i, msg))
 
           case (info, Text.Info(r0, XML.Elem(Markup(name, props), _)))
diff -r 0bc9dbc61f7f -r ad3860303ebb src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jun 29 15:53:45 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jun 29 16:16:22 2025 +0200
@@ -142,7 +142,7 @@
       model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements,
         command_states =>
           {
-            case (res, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body)))
+            case (res, Text.Info(_, msg @ XML.Elem(Markup.Bad(i), body)))
             if body.nonEmpty => Some(res + (i -> msg))
 
             case (res, Text.Info(_, msg)) =>