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 |