--- 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
}
}