# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719568306 -7200
# Node ID 80e10a1aa431984ea5020a3cbff6b0448923a772
# Parent  788b6af566ff79eeb93c507b22383f3e964fc6d7
better results view;

diff -r 788b6af566ff -r 80e10a1aa431 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Jun 28 11:33:09 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Fri Jun 28 11:51:46 2024 +0200
@@ -1109,18 +1109,20 @@
 
           build match {
             case task: Task =>
-              par(text("Task from " + task.submit_date + ". ")) ::
+              par(text("Task from " + Build_Log.print_date(task.submit_date) + ". ")) ::
               render_rev(task.isabelle_rev, task.components) :::
               render_cancel(task.uuid)
             case job: Job =>
-              par(text("Start: " + job.start_date)) ::
+              par(text("Start: " + Build_Log.print_date(job.start_date))) ::
               par(
                 if (job.cancelled) text("Cancelling...")
                 else text("Running...") ::: render_cancel(job.uuid)) ::
               render_rev(job.isabelle_rev, job.components) :::
               source(cache.lookup(store, job.kind, job.id)) :: Nil
             case result: Result =>
-              par(text("Date: " + result.start_date)) ::
+              par(text("Start: " + Build_Log.print_date(result.start_date) +
+                if_proper(result.end_date,
+                  ", took " + (result.end_date.get - result.start_date).message_hms))) ::
               par(text("Status: " + result.status)) ::
               source(cache.lookup(store, result.kind, result.id)) :: Nil
           }