src/Pure/library.scala
changeset 34317 f799f3749596
parent 34216 ada8eb23a08e
child 34320 c1509b9d624f
     1.1 --- a/src/Pure/library.scala	Mon Jan 11 20:36:31 2010 +0100
     1.2 +++ b/src/Pure/library.scala	Mon Jan 11 20:36:59 2010 +0100
     1.3 @@ -55,12 +55,13 @@
     1.4  
     1.5    /* timing */
     1.6  
     1.7 -  def timeit[A](e: => A) =
     1.8 +  def timeit[A](message: String)(e: => A) =
     1.9    {
    1.10      val start = System.currentTimeMillis()
    1.11      val result = Exn.capture(e)
    1.12      val stop = System.currentTimeMillis()
    1.13 -    System.err.println((stop - start) + "ms elapsed time")
    1.14 +    System.err.println(
    1.15 +      (if (message.isEmpty) "" else message + " ") + (stop - start) + "ms elapsed time")
    1.16      Exn.release(result)
    1.17    }
    1.18  }