# HG changeset patch
# User wenzelm
# Date 1457608283 -3600
# Node ID e31bf8ed539778114bcb1d9d38e285124a778b64
# Parent  a522a569283220dfb4e7cafe79417da11fa60b57
clarified messages, notably on Windows where CPU time of poly.exe is not measured;

diff -r a522a5692832 -r e31bf8ed5397 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Thu Mar 10 10:07:23 2016 +0100
+++ b/src/Pure/General/timing.scala	Thu Mar 10 12:11:23 2016 +0100
@@ -38,20 +38,24 @@
 
   def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
 
+  def message: String =
+    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
+
+  def resources: Time = cpu + gc
   def message_resources: String =
   {
     val resources = cpu + gc
     val t1 = elapsed.seconds
     val t2 = resources.seconds
     val factor =
-      if (t1 >= 5.0 && t2 >= 5.0)
+      if (t1 >= 3.0 && t2 >= 3.0)
         String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1))
       else ""
-    elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
+    if (t2 >= 3.0)
+      elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
+    else
+      elapsed.message_hms + " elapsed time" + factor
   }
 
-  def message: String =
-    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
-
   override def toString: String = message
 }