--- a/src/Pure/Admin/build_log.scala Wed Nov 08 21:44:44 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Wed Nov 08 21:45:02 2023 +0100
@@ -720,8 +720,8 @@
/* recent entries */
- def recent(c: SQL.Column, days: Int): PostgreSQL.Source =
- if (days <= 0) ""
+ def recent(c: SQL.Column, days: Int, default: PostgreSQL.Source = ""): PostgreSQL.Source =
+ if (days <= 0) default
else c.ident + " > now() - INTERVAL '" + days + " days'"
def recent_pull_date_table(
@@ -739,7 +739,7 @@
SQL.Table("recent_pull_date", table.columns,
table.select(table.columns, sql =
SQL.where_or(
- recent(pull_date(afp)(table), days),
+ recent(pull_date(afp)(table), days, default = SQL.TRUE),
SQL.and(eq_rev, eq_rev2))))
}
--- a/src/Pure/General/json.scala Wed Nov 08 21:44:44 2023 +0100
+++ b/src/Pure/General/json.scala Wed Nov 08 21:45:02 2023 +0100
@@ -86,7 +86,7 @@
elem("", "\"\\/".contains(_)) |
elem("", "bfnrt".contains(_)) ^^
{ case 'b' => '\b' case 'f' => '\f' case 'n' => '\n' case 'r' => '\r' case 't' => '\t' } |
- 'u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) ^^
+ 'u' ~> repeated(character(Symbol.is_ascii_hex), 4, 4) ^^
(s => Integer.parseInt(s, 16).toChar)
def string_failure: Parser[Token] = '\"' ~> failure("Unterminated string")
--- a/src/Pure/General/toml.scala Wed Nov 08 21:44:44 2023 +0100
+++ b/src/Pure/General/toml.scala Wed Nov 08 21:45:02 2023 +0100
@@ -213,8 +213,8 @@
elem("", "\"\\".contains(_)) |
elem("", "btnfr".contains(_)) ^^
{ case 'b' => '\b' case 't' => '\t' case 'n' => '\n' case 'f' => '\f' case 'r' => '\r' } |
- ('u' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 4, 4) |
- 'U' ~> repeated(character("0123456789abcdefABCDEF".contains(_)), 8, 8)) ^^
+ ('u' ~> repeated(character(Symbol.is_ascii_hex), 4, 4) |
+ 'U' ~> repeated(character(Symbol.is_ascii_hex), 8, 8)) ^^
(s => java.lang.Integer.parseInt(s, 16).toChar)
private def literal_string_elem: Parser[Elem] = elem("", c => !is_control(c) && c != '\'')