equal
deleted
inserted
replaced
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 } |