unused;

--- a/src/Pure/PIDE/markup.scala	Fri Oct 03 17:26:12 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Oct 06 16:02:52 2025 +0200
@@ -506,13 +506,6 @@
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
 
-    def unapply(props: Properties.T): Option[isabelle.Timing] =
-      (props, props, props) match {
-        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
-          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
-        case _ => None
-      }
-
     def get(props: Properties.T): isabelle.Timing = {
       val elapsed = Time.seconds(Elapsed.get(props))
       val cpu = Time.seconds(CPU.get(props))