--- a/src/Pure/System/invoke_scala.scala Thu Sep 20 16:02:10 2012 +0200
+++ b/src/Pure/System/invoke_scala.scala Thu Sep 20 19:23:05 2012 +0200
@@ -49,6 +49,7 @@
val OK = Value("1")
val ERROR = Value("2")
val FAIL = Value("3")
+ val INTERRUPT = Value("4")
}
def method(name: String, arg: String): (Tag.Value, String) =
@@ -57,6 +58,7 @@
Exn.capture { f(arg) } match {
case Exn.Res(null) => (Tag.NULL, "")
case Exn.Res(res) => (Tag.OK, res)
+ case Exn.Exn(_: InterruptedException) => (Tag.INTERRUPT, "")
case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
}
case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))