src/Pure/System/scala.scala
changeset 73702 7202e12cb324
parent 73576 b50f8cc8c08e
child 73987 fc363a3b690a
equal deleted inserted replaced
73701:d83e7e444b43 73702:7202e12cb324
    67         seconds match {
    67         seconds match {
    68           case Value.Double(s) => Time.seconds(s)
    68           case Value.Double(s) => Time.seconds(s)
    69           case _ => error("Malformed argument: " + quote(seconds))
    69           case _ => error("Malformed argument: " + quote(seconds))
    70         }
    70         }
    71       val t0 = Time.now()
    71       val t0 = Time.now()
    72       t.sleep
    72       t.sleep()
    73       val t1 = Time.now()
    73       val t1 = Time.now()
    74       (t1 - t0).toString
    74       (t1 - t0).toString
    75     }
    75     }
    76   }
    76   }
    77 
    77