diff -r f4c96158a3b8 -r 2fd90993a928 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Wed Mar 09 16:40:39 2016 +0100
+++ b/src/Pure/General/timing.scala	Wed Mar 09 16:42:30 2016 +0100
@@ -8,6 +8,9 @@
 package isabelle
 
 
+import java.util.Locale
+
+
 object Timing
 {
   val zero = Timing(Time.zero, Time.zero, Time.zero)
@@ -35,9 +38,20 @@
 
   def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.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)
+        String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1))
+      else ""
+    elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
+  }
+
   def message: String =
     elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
 
   override def toString: String = message
 }
-