summaryrefslogtreecommitdiff
path: root/src/library/scala/compat/Platform.scala
diff options
context:
space:
mode:
authormihaylov <mihaylov@epfl.ch>2006-10-24 14:06:06 +0000
committermihaylov <mihaylov@epfl.ch>2006-10-24 14:06:06 +0000
commit7e705baa349c3fc00c6ac9a5da60db4121944d5c (patch)
tree2e3f6afcb8b64e998fe4b4b32d61c5f0d6d3dcd1 /src/library/scala/compat/Platform.scala
parent2f5a1ddcde2ec8150b0fafec755b9f8bf14a65d6 (diff)
downloadscala-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.scala13
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());
}