# HG changeset patch
# User wenzelm
# Date 1693323601 -7200
# Node ID 7b80cc4701c22834f43585b8682ac6d6b153f7a5
# Parent  fd1fec53665b63b9b6ad78e4728f04dcf8565ff9
clarified signature: prefer enum types;

diff -r fd1fec53665b -r 7b80cc4701c2 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue Aug 29 17:29:34 2023 +0200
+++ b/src/Pure/System/progress.scala	Tue Aug 29 17:40:01 2023 +0200
@@ -18,9 +18,9 @@
 
   sealed abstract class Output { def message: Message }
 
-  object Kind extends Enumeration { val writeln, warning, error_message = Value }
+  enum Kind { case writeln, warning, error_message }
   sealed case class Message(
-    kind: Kind.Value,
+    kind: Kind,
     text: String,
     verbose: Boolean = false
   ) extends Output {
@@ -157,7 +157,7 @@
         SortedMap.from[Long, Message],
         { res =>
           val serial = res.long(Messages.serial)
-          val kind = Kind(res.int(Messages.kind))
+          val kind = Kind.fromOrdinal(res.int(Messages.kind))
           val text = res.string(Messages.text)
           val verbose = res.bool(Messages.verbose)
           serial -> Message(kind, text, verbose = verbose)
@@ -173,7 +173,7 @@
         for ((serial, message) <- messages) yield { (stmt: SQL.Statement) =>
           stmt.long(1) = context
           stmt.long(2) = serial
-          stmt.int(3) = message.kind.id
+          stmt.int(3) = message.kind.ordinal
           stmt.string(4) = message.text
           stmt.bool(5) = message.verbose
         })