src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Fri Sep 19 14:01:41 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Sep 20 16:34:32 2025 +0200
@@ -521,12 +521,6 @@
 
   object Timing {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
-
-    def unapply(markup: Markup): Option[isabelle.Timing] =
-      markup match {
-        case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
-        case _ => None
-      }
   }