diff -r 9f90c4864e55 -r 788b6af566ff src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Fri Jun 28 11:09:04 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Fri Jun 28 11:33:09 2024 +0200 @@ -1027,6 +1027,13 @@ main(chapter(name) :: body ::: Nil) :: Nil } + private def summary(start: Date): XML.Body = + text(" running since " + Build_Log.print_date(start)) + + private def summary(status: Status, start: Date, end: Option[Date]): XML.Body = + text(" (" + status.toString + if_proper(end, " in " + (end.get - start).message_hms) + + ") on " + Build_Log.print_date(start)) + def render_home(state: State): XML.Body = render_page("Dashboard") { def render_kind(kind: String): XML.Elem = { val running = state.get_running(kind).sortBy(_.id).reverse @@ -1036,18 +1043,17 @@ val (failed, rest) = finished.span(_.status != Status.ok) val first_failed = failed.lastOption.map(result => par( - text("first failure: ") ::: - link_build(result.name, result.id) :: - text(" on " + result.start_date))) + text("first failure: ") ::: link_build(result.name, result.id) :: + summary(result.status, result.start_date, result.end_date))) val last_success = rest.headOption.map(result => par( text("last success: ") ::: link_build(result.name, result.id) :: - text(" on " + result.start_date))) + summary(result.status, result.start_date, result.end_date))) first_failed.toList ::: last_success.toList } def render_job(job: Job): XML.Body = - par(link_build(job.name, job.id) :: text(": running since " + job.start_date)) :: + par(link_build(job.name, job.id) :: summary(job.start_date)) :: render_if( finished.headOption.exists(_.status != Status.ok) && job.kind != User_Build.name, render_previous(finished)) @@ -1055,7 +1061,7 @@ def render_result(result: Result): XML.Body = par( link_build(result.name, result.id) :: - text(" (" + result.status.toString + ") on " + result.start_date)) :: + summary(result.status, result.start_date, result.end_date)) :: render_if(result.status != Status.ok && result.kind != User_Build.name, render_previous(finished.tail)) @@ -1074,12 +1080,12 @@ def render_overview(kind: String, state: State): XML.Body = render_page("Overview: " + kind + " job ") { def render_job(job: Job): XML.Body = - List(par(link_build(job.name, job.id) :: text(" running since " + job.start_date))) + List(par(link_build(job.name, job.id) :: summary(job.start_date))) def render_result(result: Result): XML.Body = List(par( link_build(result.name, result.id) :: - text(" (" + result.status + ") on " + result.start_date))) + summary(result.status, result.start_date, result.end_date))) itemize( state.get_running(kind).sortBy(_.id).reverse.map(render_job) :::