# HG changeset patch
# User wenzelm
# Date 1396361785 -7200
# Node ID 1c735e46acf08f10ae823a29485880e851c6dc55
# Parent  949d4c7a86c63b627dfa3eab177f92b8a0a7e293
simplified using "value class";

diff -r 949d4c7a86c6 -r 1c735e46acf0 src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Tue Apr 01 11:02:40 2014 +0200
+++ b/src/Pure/General/time.scala	Tue Apr 01 16:16:25 2014 +0200
@@ -21,7 +21,7 @@
     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
 }
 
-final class Time private(val ms: Long)
+final class Time private(val ms: Long) extends AnyVal
 {
   def + (t: Time): Time = new Time(ms + t.ms)
 
@@ -33,13 +33,6 @@
   def is_zero: Boolean = ms == 0
   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"