src/Pure/PIDE/document_status.scala
changeset 83294 8d30612cff2d
parent 83289 2cd87a6da20b
child 83296 405ccae51c72
--- a/src/Pure/PIDE/document_status.scala	Thu Oct 16 12:31:15 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Thu Oct 16 14:31:35 2025 +0200
@@ -179,7 +179,7 @@
           case Markup.WARNING | Markup.LEGACY => warned1 = true
           case Markup.FAILED | Markup.ERROR => failed1 = true
           case Markup.CANCELED => canceled1 = true
-          case Markup.TIMING =>
+          case Markup.Command_Timing.name =>
             val props = markup.properties
             val offset = Position.Offset.get(props)
             val t = Time.seconds(Markup.Elapsed.get(props))