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