diff -r 0bbbf8e26708 -r 7bfac764a715 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Tue Aug 29 17:06:24 2023 +0200
+++ b/src/Pure/System/scala.scala	Tue Aug 29 17:10:48 2023 +0200
@@ -102,11 +102,10 @@
 
   object Compiler {
     object Message {
-      object Kind extends Enumeration {
-        val error, warning, info, other = Value
-      }
+      enum Kind { case error, warning, info, other }
+
       private val Header = """^--.* (Error|Warning|Info): .*$""".r
-      val header_kind: String => Kind.Value =
+      val header_kind: String => Kind =
         {
           case "Error" => Kind.error
           case "Warning" => Kind.warning
@@ -139,7 +138,7 @@
       }
     }
 
-    sealed case class Message(kind: Message.Kind.Value, text: String)
+    sealed case class Message(kind: Message.Kind, text: String)
     {
       def is_error: Boolean = kind == Message.Kind.error
       override def toString: String = text