# HG changeset patch
# User wenzelm
# Date 1475851847 -7200
# Node ID bca58a11efde1948b4d774c3976ee5a561504d9f
# Parent  fef1a0a59c126c7aa11238652e29008c4e57c24f
more operations;

diff -r fef1a0a59c12 -r bca58a11efde src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Fri Oct 07 14:17:20 2016 +0200
+++ b/src/Pure/General/timing.scala	Fri Oct 07 16:50:47 2016 +0200
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/timing.scala
-    Module:     PIDE
     Author:     Makarius
 
 Basic support for time measurement.
@@ -36,25 +35,31 @@
 {
   def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
 
+  def resources: Time = cpu + gc
+
+  def factor: Option[Double] =
+  {
+    val t1 = elapsed.seconds
+    val t2 = resources.seconds
+    if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None
+  }
+
   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 >= 3.0 && t2 >= 3.0)
-        String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1))
-      else ""
-    if (t2 >= 3.0)
-      elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
+    val factor_text =
+      factor match {
+        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f))
+        case None => ""
+      }
+    if (resources.seconds >= 3.0)
+      elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text
     else
-      elapsed.message_hms + " elapsed time" + factor
+      elapsed.message_hms + " elapsed time" + factor_text
   }
 
   override def toString: String = message