--- a/src/Pure/Admin/build_log.scala Thu Aug 25 15:30:21 2022 +0200
+++ b/src/Pure/Admin/build_log.scala Thu Aug 25 15:52:42 2022 +0200
@@ -718,7 +718,7 @@
/* recent entries */
- def recent_time(days: Int): SQL.Source =
+ def recent_time(days: Int): PostgreSQL.Source =
"now() - INTERVAL '" + days.max(0) + " days'"
def recent_pull_date_table(
@@ -744,7 +744,7 @@
else "")))
}
- def select_recent_log_names(days: Int): SQL.Source = {
+ def select_recent_log_names(days: Int): PostgreSQL.Source = {
val table1 = meta_info_table
val table2 = recent_pull_date_table(days)
table1.select(List(log_name), distinct = true) + SQL.join_inner + table2.query_named +
@@ -755,8 +755,8 @@
days: Int,
rev: String = "",
afp_rev: Option[String] = None,
- sql: SQL.Source = ""
- ): SQL.Source = {
+ sql: PostgreSQL.Source = ""
+ ): PostgreSQL.Source = {
val afp = afp_rev.isDefined
val version = Prop.isabelle_version
val table1 = recent_pull_date_table(days, rev = rev, afp_rev = afp_rev)
--- a/src/Pure/Admin/build_status.scala Thu Aug 25 15:30:21 2022 +0200
+++ b/src/Pure/Admin/build_status.scala Thu Aug 25 15:52:42 2022 +0200
@@ -36,7 +36,7 @@
options: Options,
columns: List[SQL.Column],
only_sessions: Set[String]
- ): SQL.Source = {
+ ): PostgreSQL.Source = {
Build_Log.Data.universal_table.select(columns, distinct = true,
sql = "WHERE " +
Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) +
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Aug 25 15:30:21 2022 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Aug 25 15:52:42 2022 +0200
@@ -110,7 +110,7 @@
days: Int,
rev: String,
afp_rev: Option[String],
- sql: SQL.Source
+ sql: PostgreSQL.Source
): List[Item] = {
val afp = afp_rev.isDefined
val select =
@@ -150,7 +150,7 @@
afp: Boolean = false,
bulky: Boolean = false,
more_hosts: List[String] = Nil,
- detect: SQL.Source = "",
+ detect: PostgreSQL.Source = "",
active: Boolean = true
) {
def ssh_session(context: SSH.Context): SSH.Session =
@@ -158,7 +158,7 @@
proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
permissive = proxy_host.nonEmpty)
- def sql: SQL.Source =
+ def sql: PostgreSQL.Source =
Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " +
SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
(if (detect == "") "" else " AND " + SQL.enclose(detect))