# HG changeset patch
# User wenzelm
# Date 1693321584 -7200
# Node ID 0bbbf8e26708eeac84cedd130b8b2f66fc3755ca
# Parent  9ccd5e8737cbd9bc721a7a39a654f8d8e2090dcb
clarified signature: prefer enum types;

diff -r 9ccd5e8737cb -r 0bbbf8e26708 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Tue Aug 29 17:00:12 2023 +0200
+++ b/src/Pure/System/scala.scala	Tue Aug 29 17:06:24 2023 +0200
@@ -275,9 +275,7 @@
 
   /* invoke function */
 
-  object Tag extends Enumeration {
-    val NULL, OK, ERROR, FAIL, INTERRUPT = Value
-  }
+  enum Tag { case NULL, OK, ERROR, FAIL, INTERRUPT }
 
   def function_thread(name: String): Boolean =
     functions.find(fun => fun.name == name) match {
@@ -285,7 +283,7 @@
       case None => false
     }
 
-  def function_body(session: Session, name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) =
+  def function_body(session: Session, name: String, args: List[Bytes]): (Tag, List[Bytes]) =
     functions.find(fun => fun.name == name) match {
       case Some(fun) =>
         Exn.capture { fun.invoke(session, args) } match {
@@ -312,10 +310,11 @@
       futures = Map.empty
     }
 
-    private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit =
+    private def result(id: String, tag: Scala.Tag, res: List[Bytes]): Unit =
       synchronized {
         if (futures.isDefinedAt(id)) {
-          session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res)
+          session.protocol_command_raw(
+            "Scala.result", Bytes(id) :: Bytes(tag.ordinal.toString) :: res)
           futures -= id
         }
       }