# HG changeset patch
# User nipkow
# Date 1699476302 -3600
# Node ID ab85d87dc2beb7649640d72b92be24a9bc606918
# Parent  2fee5fba3116771dc0930e4e1f89e9e57369f3ed# Parent  9e43ab263d338f586dbf968e11a1b9cf6f7162de
merged

diff -r 9e43ab263d33 -r ab85d87dc2be src/Pure/Admin/build_log.scala
--- 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))))
     }
 
diff -r 9e43ab263d33 -r ab85d87dc2be src/Pure/General/json.scala
--- 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")
diff -r 9e43ab263d33 -r ab85d87dc2be src/Pure/General/toml.scala
--- 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 != '\'')