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