src/Pure/System/invoke_scala.scala
changeset 49470 ee564db2649b
parent 49173 fa01a202399c
child 52111 1fd184eaa310
--- 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))