changeset 68806 | 4597812d5182 |
parent 68315 | d088799fd278 |
child 71142 | d6688677a784 |
--- a/src/Pure/General/exn.scala Sat Aug 25 17:20:06 2018 +0200 +++ b/src/Pure/General/exn.scala Sat Aug 25 20:10:49 2018 +0200 @@ -138,4 +138,10 @@ def message(exn: Throwable): String = user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString) + + + /* trace */ + + def trace(exn: Throwable): String = + exn.getStackTrace.mkString("\n") }