src/Pure/Build/build_manager.scala
changeset 80419 788b6af566ff
parent 80416 c369b0419172
child 80420 80e10a1aa431
equal deleted inserted replaced
80418:9f90c4864e55 80419:788b6af566ff
  1025 
  1025 
  1026         More_HTML.header(List(nav(List(nav_link(Page.HOME, "home"))))) ::
  1026         More_HTML.header(List(nav(List(nav_link(Page.HOME, "home"))))) ::
  1027         main(chapter(name) :: body ::: Nil) :: Nil
  1027         main(chapter(name) :: body ::: Nil) :: Nil
  1028       }
  1028       }
  1029 
  1029 
       
  1030       private def summary(start: Date): XML.Body =
       
  1031         text(" running since " + Build_Log.print_date(start))
       
  1032 
       
  1033       private def summary(status: Status, start: Date, end: Option[Date]): XML.Body =
       
  1034         text(" (" + status.toString + if_proper(end, " in " + (end.get - start).message_hms) +
       
  1035           ") on " + Build_Log.print_date(start))
       
  1036 
  1030       def render_home(state: State): XML.Body = render_page("Dashboard") {
  1037       def render_home(state: State): XML.Body = render_page("Dashboard") {
  1031         def render_kind(kind: String): XML.Elem = {
  1038         def render_kind(kind: String): XML.Elem = {
  1032           val running = state.get_running(kind).sortBy(_.id).reverse
  1039           val running = state.get_running(kind).sortBy(_.id).reverse
  1033           val finished = state.get_finished(kind).sortBy(_.id).reverse
  1040           val finished = state.get_finished(kind).sortBy(_.id).reverse
  1034 
  1041 
  1035           def render_previous(finished: List[Result]): XML.Body = {
  1042           def render_previous(finished: List[Result]): XML.Body = {
  1036             val (failed, rest) = finished.span(_.status != Status.ok)
  1043             val (failed, rest) = finished.span(_.status != Status.ok)
  1037             val first_failed = failed.lastOption.map(result =>
  1044             val first_failed = failed.lastOption.map(result =>
  1038               par(
  1045               par(
  1039                 text("first failure: ") :::
  1046                 text("first failure: ") ::: link_build(result.name, result.id) ::
  1040                 link_build(result.name, result.id) ::
  1047                 summary(result.status, result.start_date, result.end_date)))
  1041                 text(" on " + result.start_date)))
       
  1042             val last_success = rest.headOption.map(result =>
  1048             val last_success = rest.headOption.map(result =>
  1043               par(
  1049               par(
  1044                 text("last success: ") ::: link_build(result.name, result.id) ::
  1050                 text("last success: ") ::: link_build(result.name, result.id) ::
  1045                 text(" on " + result.start_date)))
  1051                 summary(result.status, result.start_date, result.end_date)))
  1046             first_failed.toList ::: last_success.toList
  1052             first_failed.toList ::: last_success.toList
  1047           }
  1053           }
  1048 
  1054 
  1049           def render_job(job: Job): XML.Body =
  1055           def render_job(job: Job): XML.Body =
  1050             par(link_build(job.name, job.id) :: text(": running since " + job.start_date)) ::
  1056             par(link_build(job.name, job.id) :: summary(job.start_date)) ::
  1051             render_if(
  1057             render_if(
  1052               finished.headOption.exists(_.status != Status.ok) && job.kind != User_Build.name,
  1058               finished.headOption.exists(_.status != Status.ok) && job.kind != User_Build.name,
  1053               render_previous(finished))
  1059               render_previous(finished))
  1054 
  1060 
  1055           def render_result(result: Result): XML.Body =
  1061           def render_result(result: Result): XML.Body =
  1056             par(
  1062             par(
  1057               link_build(result.name, result.id) ::
  1063               link_build(result.name, result.id) ::
  1058               text(" (" + result.status.toString + ") on " + result.start_date)) ::
  1064               summary(result.status, result.start_date, result.end_date)) ::
  1059             render_if(result.status != Status.ok && result.kind != User_Build.name,
  1065             render_if(result.status != Status.ok && result.kind != User_Build.name,
  1060               render_previous(finished.tail))
  1066               render_previous(finished.tail))
  1061 
  1067 
  1062           fieldset(
  1068           fieldset(
  1063             XML.elem("legend", List(link_kind(kind))) ::
  1069             XML.elem("legend", List(link_kind(kind))) ::
  1072       }
  1078       }
  1073 
  1079 
  1074       def render_overview(kind: String, state: State): XML.Body =
  1080       def render_overview(kind: String, state: State): XML.Body =
  1075         render_page("Overview: " + kind + " job ") {
  1081         render_page("Overview: " + kind + " job ") {
  1076           def render_job(job: Job): XML.Body =
  1082           def render_job(job: Job): XML.Body =
  1077             List(par(link_build(job.name, job.id) :: text(" running since " + job.start_date)))
  1083             List(par(link_build(job.name, job.id) :: summary(job.start_date)))
  1078 
  1084 
  1079           def render_result(result: Result): XML.Body =
  1085           def render_result(result: Result): XML.Body =
  1080             List(par(
  1086             List(par(
  1081               link_build(result.name, result.id) ::
  1087               link_build(result.name, result.id) ::
  1082               text(" (" + result.status + ") on " + result.start_date)))
  1088               summary(result.status, result.start_date, result.end_date)))
  1083 
  1089 
  1084           itemize(
  1090           itemize(
  1085             state.get_running(kind).sortBy(_.id).reverse.map(render_job) :::
  1091             state.get_running(kind).sortBy(_.id).reverse.map(render_job) :::
  1086             state.get_finished(kind).sortBy(_.id).reverse.map(render_result)) :: Nil
  1092             state.get_finished(kind).sortBy(_.id).reverse.map(render_result)) :: Nil
  1087         }
  1093         }