diff -r 4161a5a38f2a -r 8d30612cff2d src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Oct 16 12:31:15 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Oct 16 14:31:35 2025 +0200
@@ -514,8 +514,6 @@
     }
   }
 
-  val TIMING = "timing"
-
 
   /* process result */