src/Pure/General/time.scala

--- a/src/Pure/General/time.scala	Wed Mar 09 16:40:39 2016 +0100
+++ b/src/Pure/General/time.scala	Wed Mar 09 16:42:30 2016 +0100
@@ -46,5 +46,11 @@
   override def toString: String = Time.print_seconds(seconds)
 
   def message: String = toString + "s"
+
+  def message_hms: String =
+  {
+    val s = ms / 1000
+    String.format(Locale.ROOT, "%d:%02d:%02d",
+      new java.lang.Long(s / 3600), new java.lang.Long((s / 60) % 60), new java.lang.Long(s % 60))
+  }
 }
-