diff options
author | mihaylov <mihaylov@epfl.ch> | 2006-10-24 14:06:06 +0000 |
---|---|---|
committer | mihaylov <mihaylov@epfl.ch> | 2006-10-24 14:06:06 +0000 |
commit | 7e705baa349c3fc00c6ac9a5da60db4121944d5c (patch) | |
tree | 2e3f6afcb8b64e998fe4b4b32d61c5f0d6d3dcd1 /src/library/scala/compat/Platform.scala | |
parent | 2f5a1ddcde2ec8150b0fafec755b9f8bf14a65d6 (diff) | |
download | scala-7e705baa349c3fc00c6ac9a5da60db4121944d5c.tar.gz scala-7e705baa349c3fc00c6ac9a5da60db4121944d5c.tar.bz2 scala-7e705baa349c3fc00c6ac9a5da60db4121944d5c.zip |
Mapped Java exceptions via scala.compat.Platform
Diffstat (limited to 'src/library/scala/compat/Platform.scala')
-rw-r--r-- | src/library/scala/compat/Platform.scala | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/library/scala/compat/Platform.scala b/src/library/scala/compat/Platform.scala index 9a579af2a1..08aa1f1188 100644 --- a/src/library/scala/compat/Platform.scala +++ b/src/library/scala/compat/Platform.scala @@ -20,6 +20,9 @@ object Platform { type ClassCastException = java.lang.ClassCastException; type RuntimeException = java.lang.RuntimeException; type IndexOutOfBoundsException = java.lang.IndexOutOfBoundsException; + type UnsupportedOperationException = java.lang.UnsupportedOperationException + type IllegalArgumentException = java.lang.IllegalArgumentException + type NoSuchElementException = java.util.NoSuchElementException def arraycopy(src: AnyRef, srcPos: Int, dest: AnyRef, destPos: Int, length: Int): Unit = Array.copy(src, srcPos, dest, destPos, length) @@ -36,6 +39,16 @@ object Platform { def printStackTrace(exc: java.lang.Throwable) = exc.printStackTrace(); def getMessage(exc: java.lang.Throwable) = exc.getMessage(); + private val eol = System.getProperty("line.separator", "\n") + def getStackTrace(exc: java.lang.Throwable): String = { + val s = new StringBuilder() + for (val trElem <- exc.getStackTrace()) { + s.append(trElem.toString()) + s.append(eol) + } + s.toString() + } + def split(str: String, separator: Char): Array[String] = { str.split(separator.toString()); } |