more operations on Time, Timing;

--- 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"

--- a/src/Pure/General/timing.scala	Sat Mar 30 14:57:06 2013 +0100
+++ b/src/Pure/General/timing.scala	Sat Mar 30 16:15:26 2013 +0100
@@ -10,6 +10,8 @@
 
 object Timing
 {
+  val zero = Timing(Time.zero, Time.zero, Time.zero)
+
   def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
     if (enabled) {
       val start = java.lang.System.currentTimeMillis()
@@ -27,10 +29,12 @@
     else e
 }
 
-class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
+sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
 {
   def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
 
+  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"