src/Pure/General/time.scala

--- a/src/Pure/General/time.scala	Fri Apr 28 18:11:40 2017 +0200
+++ b/src/Pure/General/time.scala	Fri Apr 28 18:23:39 2017 +0200
@@ -34,6 +34,8 @@
 
 final class Time private(val ms: Long) extends AnyVal
 {
+  def proper_ms: Option[Long] = if (ms == 0) None else Some(ms)
+
   def seconds: Double = ms / 1000.0
   def minutes: Double = ms / 60000.0