# HG changeset patch # User wenzelm # Date 1686736063 -7200 # Node ID 55a6aa77f3d8f8126dcf9f1e593fe4d6858a7206 # Parent d4f387339494d7bd523055400f66c4492ebcca9a tuned signature: more operations; diff -r d4f387339494 -r 55a6aa77f3d8 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Wed Jun 14 11:18:25 2023 +0200 +++ b/src/Pure/Admin/build_log.scala Wed Jun 14 11:47:43 2023 +0200 @@ -686,7 +686,7 @@ val version2 = Prop.afp_version build_log_table("isabelle_afp_versions", List(version1.make_primary_key, version2), SQL.select(List(version1, version2), distinct = true) + meta_info_table + - SQL.where(SQL.and(version1.defined, version2.defined))) + SQL.where_and(version1.defined, version2.defined)) } @@ -729,9 +729,9 @@ SQL.Table("recent_pull_date", table.columns, table.select(table.columns, sql = - SQL.where( - SQL.or(pull_date(afp)(table).ident + " > " + recent_time(days), - SQL.and(eq_rev, eq_rev2))))) + SQL.where_or( + pull_date(afp)(table).ident + " > " + recent_time(days), + SQL.and(eq_rev, eq_rev2)))) } def select_recent_log_names(days: Int): PostgreSQL.Source = { @@ -1102,11 +1102,10 @@ else (columns1, table1.ident) val where = - SQL.where( - SQL.and( - Data.log_name(table1).equal(log_name), - Data.session_name(table1).ident + " <> ''", - if_proper(session_names, Data.session_name(table1).member(session_names)))) + SQL.where_and( + Data.log_name(table1).equal(log_name), + Data.session_name(table1).ident + " <> ''", + if_proper(session_names, Data.session_name(table1).member(session_names))) val sessions = db.execute_query_statement( diff -r d4f387339494 -r 55a6aa77f3d8 src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Wed Jun 14 11:18:25 2023 +0200 +++ b/src/Pure/Admin/build_status.scala Wed Jun 14 11:47:43 2023 +0200 @@ -61,15 +61,14 @@ (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil) Build_Log.Data.universal_table.select(columns, distinct = true, sql = - SQL.where( - SQL.and( - Build_Log.Data.pull_date(afp).ident + " > " + Build_Log.Data.recent_time(days(options)), - Build_Log.Data.status.member( - List( - Build_Log.Session_Status.finished.toString, - Build_Log.Session_Status.failed.toString)), - if_proper(only_sessions, Build_Log.Data.session_name.member(only_sessions)), - if_proper(sql, SQL.enclose(sql))))) + SQL.where_and( + Build_Log.Data.pull_date(afp).ident + " > " + Build_Log.Data.recent_time(days(options)), + Build_Log.Data.status.member( + List( + Build_Log.Session_Status.finished.toString, + Build_Log.Session_Status.failed.toString)), + if_proper(only_sessions, Build_Log.Data.session_name.member(only_sessions)), + if_proper(sql, SQL.enclose(sql)))) } } diff -r d4f387339494 -r 55a6aa77f3d8 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Wed Jun 14 11:18:25 2023 +0200 +++ b/src/Pure/General/sql.scala Wed Jun 14 11:47:43 2023 +0200 @@ -81,6 +81,8 @@ else OR(set.iterator.map(equal(sql, _)).toList) def where(sql: Source): Source = if_proper(sql, " WHERE " + sql) + def where_and(args: Source*): Source = where(and(args:_*)) + def where_or(args: Source*): Source = where(or(args:_*)) /* types */ diff -r d4f387339494 -r 55a6aa77f3d8 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Wed Jun 14 11:18:25 2023 +0200 +++ b/src/Pure/Thy/document_build.scala Wed Jun 14 11:47:43 2023 +0200 @@ -64,10 +64,9 @@ val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) def where_equal(session_name: String, name: String = ""): SQL.Source = - SQL.where( - SQL.and( - Data.session_name.equal(session_name), - if_proper(name, Data.name.equal(name)))) + SQL.where_and( + Data.session_name.equal(session_name), + if_proper(name, Data.name.equal(name))) } def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = diff -r d4f387339494 -r 55a6aa77f3d8 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Wed Jun 14 11:18:25 2023 +0200 +++ b/src/Pure/Thy/export.scala Wed Jun 14 11:47:43 2023 +0200 @@ -44,11 +44,10 @@ val tables = SQL.Tables(table) def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source = - SQL.where( - SQL.and( - Data.session_name.equal(session_name), - if_proper(theory_name, Data.theory_name.equal(theory_name)), - if_proper(name, Data.name.equal(name)))) + SQL.where_and( + Data.session_name.equal(session_name), + if_proper(theory_name, Data.theory_name.equal(theory_name)), + if_proper(name, Data.name.equal(name))) } def compound_name(a: String, b: String): String = diff -r d4f387339494 -r 55a6aa77f3d8 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Jun 14 11:18:25 2023 +0200 +++ b/src/Pure/Thy/sessions.scala Wed Jun 14 11:47:43 2023 +0200 @@ -119,10 +119,9 @@ SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body)) def where_equal(session_name: String, name: String = ""): SQL.Source = - SQL.where( - SQL.and( - Sources.session_name.equal(session_name), - if_proper(name, Sources.name.equal(name)))) + SQL.where_and( + Sources.session_name.equal(session_name), + if_proper(name, Sources.name.equal(name))) def load(session_base: Base, cache: Compress.Cache = Compress.Cache.none): Sources = new Sources( diff -r d4f387339494 -r 55a6aa77f3d8 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Wed Jun 14 11:18:25 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Wed Jun 14 11:47:43 2023 +0200 @@ -499,10 +499,9 @@ db.execute_query_statement( Progress.table.select( sql = - SQL.where( - SQL.and( - if (seen <= 0) "" else Progress.serial.ident + " > " + seen, - Generic.sql(build_uuid = build_uuid)))), + SQL.where_and( + if (seen <= 0) "" else Progress.serial.ident + " > " + seen, + Generic.sql(build_uuid = build_uuid))), SortedMap.from[Long, isabelle.Progress.Message], { res => val serial = res.long(Progress.serial)