src/Pure/library.scala
changeset 34314 f799f3749596
parent 34216 ada8eb23a08e
child 34317 c1509b9d624f
equal deleted inserted replaced
34313:2f890016afab 34314:f799f3749596
    53   def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
    53   def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
    54 
    54 
    55 
    55 
    56   /* timing */
    56   /* timing */
    57 
    57 
    58   def timeit[A](e: => A) =
    58   def timeit[A](message: String)(e: => A) =
    59   {
    59   {
    60     val start = System.currentTimeMillis()
    60     val start = System.currentTimeMillis()
    61     val result = Exn.capture(e)
    61     val result = Exn.capture(e)
    62     val stop = System.currentTimeMillis()
    62     val stop = System.currentTimeMillis()
    63     System.err.println((stop - start) + "ms elapsed time")
    63     System.err.println(
       
    64       (if (message.isEmpty) "" else message + " ") + (stop - start) + "ms elapsed time")
    64     Exn.release(result)
    65     Exn.release(result)
    65   }
    66   }
    66 }
    67 }