--- a/Admin/components/components.sha1 Fri Apr 01 10:55:32 2022 +0200
+++ b/Admin/components/components.sha1 Fri Apr 01 11:18:03 2022 +0200
@@ -398,6 +398,7 @@
201c05ae9cc382ee6c08af49430e426f6bbe0d5a scala-2.12.8.tar.gz
a0622fe75c3482ba7dc3ce74d58583b648a1ff0d scala-2.13.4-1.tar.gz
ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
+caedd48ae65db9d116a0e1712eec3a66fe95c712 scala-2.13.5-1.tar.gz
f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz
0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz
1f8532dba290c6b2ef364632f3f92e71da93baba scala-2.13.7.tar.gz
--- a/Admin/components/main Fri Apr 01 10:55:32 2022 +0200
+++ b/Admin/components/main Fri Apr 01 11:18:03 2022 +0200
@@ -21,7 +21,7 @@
pdfjs-2.12.313
polyml-test-15c840d48c9a
postgresql-42.2.24
-scala-2.13.5
+scala-2.13.5-1
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.36.0.3
--- a/src/Pure/Isar/token.scala Fri Apr 01 10:55:32 2022 +0200
+++ b/src/Pure/Isar/token.scala Fri Apr 01 11:18:03 2022 +0200
@@ -89,8 +89,8 @@
(x => Token(Token.Kind.SYM_IDENT, x))
val keyword =
- literal(keywords.minor) ^^ (x => Token(Token.Kind.KEYWORD, x)) |||
- literal(keywords.major) ^^ (x => Token(Token.Kind.COMMAND, x))
+ literal(keywords.major) ^^ (x => Token(Token.Kind.COMMAND, x)) |||
+ literal(keywords.minor) ^^ (x => Token(Token.Kind.KEYWORD, x))
val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
@@ -102,8 +102,8 @@
val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x))
space | (recover_delimited |
- (((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
- keyword) | bad))
+ ((keyword |||
+ (ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident))))))) | bad))
}
def token(keywords: Keyword.Keywords): Parser[Token] =
--- a/src/Pure/ML/ml_lex.scala Fri Apr 01 10:55:32 2022 +0200
+++ b/src/Pure/ML/ml_lex.scala Fri Apr 01 11:18:03 2022 +0200
@@ -249,7 +249,7 @@
(x => Token(Kind.ERROR, x))
space | (ml_control | (recover | (ml_antiq |
- (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))))
+ ((keyword ||| (word | (real | (int | (long_ident | (ident | type_var)))))) | bad))))
}
def token: Parser[Token] =