src/Pure/Build/build_manager.scala
changeset 80420 80e10a1aa431
parent 80419 788b6af566ff
child 80421 96e1b4f38a17
equal deleted inserted replaced
80419:788b6af566ff 80420:80e10a1aa431
  1107               if !component.is_local
  1107               if !component.is_local
  1108             } yield par(text(component.toString))
  1108             } yield par(text(component.toString))
  1109 
  1109 
  1110           build match {
  1110           build match {
  1111             case task: Task =>
  1111             case task: Task =>
  1112               par(text("Task from " + task.submit_date + ". ")) ::
  1112               par(text("Task from " + Build_Log.print_date(task.submit_date) + ". ")) ::
  1113               render_rev(task.isabelle_rev, task.components) :::
  1113               render_rev(task.isabelle_rev, task.components) :::
  1114               render_cancel(task.uuid)
  1114               render_cancel(task.uuid)
  1115             case job: Job =>
  1115             case job: Job =>
  1116               par(text("Start: " + job.start_date)) ::
  1116               par(text("Start: " + Build_Log.print_date(job.start_date))) ::
  1117               par(
  1117               par(
  1118                 if (job.cancelled) text("Cancelling...")
  1118                 if (job.cancelled) text("Cancelling...")
  1119                 else text("Running...") ::: render_cancel(job.uuid)) ::
  1119                 else text("Running...") ::: render_cancel(job.uuid)) ::
  1120               render_rev(job.isabelle_rev, job.components) :::
  1120               render_rev(job.isabelle_rev, job.components) :::
  1121               source(cache.lookup(store, job.kind, job.id)) :: Nil
  1121               source(cache.lookup(store, job.kind, job.id)) :: Nil
  1122             case result: Result =>
  1122             case result: Result =>
  1123               par(text("Date: " + result.start_date)) ::
  1123               par(text("Start: " + Build_Log.print_date(result.start_date) +
       
  1124                 if_proper(result.end_date,
       
  1125                   ", took " + (result.end_date.get - result.start_date).message_hms))) ::
  1124               par(text("Status: " + result.status)) ::
  1126               par(text("Status: " + result.status)) ::
  1125               source(cache.lookup(store, result.kind, result.id)) :: Nil
  1127               source(cache.lookup(store, result.kind, result.id)) :: Nil
  1126           }
  1128           }
  1127         }
  1129         }
  1128 
  1130