# HG changeset patch
# User wenzelm
# Date 1493490886 -7200
# Node ID f86798cbe0c26dbc403cdce4c3450a0234134ffb
# Parent  e9b87bf6578b76e04b87d7407f05cecc9c9bcc7a
tuned;

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