--- 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))