diff -r e9b87bf6578b -r f86798cbe0c2 src/Pure/System/invoke_scala.scala --- a/src/Pure/System/invoke_scala.scala Sat Apr 29 20:30:13 2017 +0200 +++ b/src/Pure/System/invoke_scala.scala Sat Apr 29 20:34:46 2017 +0200 @@ -46,11 +46,7 @@ object Tag extends Enumeration { - val NULL = Value("0") - val OK = Value("1") - val ERROR = Value("2") - val FAIL = Value("3") - val INTERRUPT = Value("4") + val NULL, OK, ERROR, FAIL, INTERRUPT = Value } def method(name: String, arg: String): (Tag.Value, String) = @@ -87,7 +83,7 @@ synchronized { if (futures.isDefinedAt(id)) { - session.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res) + session.protocol_command("Invoke_Scala.fulfill", id, tag.id.toString, res) futures -= id } }