src/Pure/General/time.scala

--- a/src/Pure/General/time.scala	Sat Mar 30 14:57:06 2013 +0100
+++ b/src/Pure/General/time.scala	Sat Mar 30 16:15:26 2013 +0100
@@ -15,6 +15,7 @@
 {
   def seconds(s: Double): Time = new Time((s * 1000.0).round)
   def ms(m: Long): Time = new Time(m)
+  val zero: Time = ms(0)
 
   def print_seconds(s: Double): String =
     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
@@ -22,6 +23,8 @@
 
 final class Time private(val ms: Long)
 {
+  def + (t: Time): Time = new Time(ms + t.ms)
+
   def seconds: Double = ms / 1000.0
 
   def min(t: Time): Time = if (ms < t.ms) this else t
@@ -29,6 +32,13 @@
 
   def is_relevant: Boolean = ms >= 1
 
+  override def hashCode: Int = ms.hashCode
+  override def equals(that: Any): Boolean =
+    that match {
+      case other: Time => ms == other.ms
+      case _ => false
+    }
+
   override def toString = Time.print_seconds(seconds)
 
   def message: String = toString + "s"