# HG changeset patch
# User wenzelm
# Date 1693322359 -7200
# Node ID 67492b2a3a626b16d133a7c228998fe8e2ca7084
# Parent  0e01c3b55b63769e0344859e9b5fe38ef71aa472
clarified signature: prefer enum types;

diff -r 0e01c3b55b63 -r 67492b2a3a62 src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Tue Aug 29 17:17:12 2023 +0200
+++ b/src/Pure/General/toml.scala	Tue Aug 29 17:19:19 2023 +0200
@@ -133,11 +133,9 @@
 
   /* lexer */
 
-  object Kind extends Enumeration {
-    val KEYWORD, VALUE, STRING, MULTILINE_STRING, LINE_SEP, ERROR = Value
-  }
+  enum Kind { case KEYWORD, VALUE, STRING, MULTILINE_STRING, LINE_SEP, ERROR }
 
-  sealed case class Token(kind: Kind.Value, text: Str) {
+  sealed case class Token(kind: Kind, text: Str) {
     def is_keyword(name: Str): Bool = kind == Kind.KEYWORD && text == name
     def is_value: Bool = kind == Kind.VALUE
     def is_string: Bool = kind == Kind.STRING