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