# HG changeset patch
# User wenzelm
# Date 1693318709 -7200
# Node ID ecf0b65ada9ed20b12cc4800d600e6bf3db2e789
# Parent  470d4f1e89d9f3a3b13ef83670832c7f5a5440b7
clarified signature: prefer enum types;

diff -r 470d4f1e89d9 -r ecf0b65ada9e src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Tue Aug 29 15:49:19 2023 +0200
+++ b/src/Pure/General/json.scala	Tue Aug 29 16:18:29 2023 +0200
@@ -41,11 +41,9 @@
 
   /* lexer */
 
-  object Kind extends Enumeration {
-    val KEYWORD, STRING, NUMBER, ERROR = this.Value
-  }
+  enum Kind { case KEYWORD, STRING, NUMBER, ERROR }
 
-  sealed case class Token(kind: Kind.Value, text: String) {
+  sealed case class Token(kind: Kind, text: String) {
     def is_keyword: Boolean = kind == Kind.KEYWORD
     def is_keyword(name: String): Boolean = kind == Kind.KEYWORD && text == name
     def is_string: Boolean = kind == Kind.STRING