# HG changeset patch # User wenzelm # Date 1677331999 -3600 # Node ID 47c2ac81ddd4b90ddecf742595e71f68b582e4f9 # Parent df17355f1e2c8fe0a999c1a7d813bbc4bd2e9e80 clarified signature: more robust operations; diff -r df17355f1e2c -r 47c2ac81ddd4 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Fri Feb 24 20:52:35 2023 +0100 +++ b/src/Pure/Admin/build_log.scala Sat Feb 25 14:33:19 2023 +0100 @@ -681,7 +681,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 + - " WHERE " + version1.defined + " AND " + version2.defined) + SQL.where(SQL.and(version1.defined, version2.defined))) } @@ -700,7 +700,7 @@ "SELECT " + versions.mkString(", ") + ", min(" + Prop.build_start + ") AS " + pull_date(afp) + " FROM " + meta_info_table + - " WHERE " + (versions ::: List(Prop.build_start)).map(_.defined).mkString(" AND ") + + " WHERE " + SQL.AND((versions ::: List(Prop.build_start)).map(_.defined)) + " GROUP BY " + versions.mkString(", ")) } diff -r df17355f1e2c -r 47c2ac81ddd4 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Fri Feb 24 20:52:35 2023 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sat Feb 25 14:33:19 2023 +0100 @@ -155,9 +155,10 @@ SSH.open_session(options, host = host, user = user, port = port) 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_proper(detect, " AND " + SQL.enclose(detect)) + SQL.and( + Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine), + SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts), + if_proper(detect, SQL.enclose(detect))) def profile: Build_Status.Profile = Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql) diff -r df17355f1e2c -r 47c2ac81ddd4 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Fri Feb 24 20:52:35 2023 +0100 +++ b/src/Pure/General/sql.scala Sat Feb 25 14:33:19 2023 +0100 @@ -55,12 +55,29 @@ val join_inner: Source = " INNER JOIN " def join(outer: Boolean): Source = if (outer) join_outer else join_inner + def infix(op: Source, args: Iterable[Source]): Source = { + val body = args.iterator.filter(_.nonEmpty).mkString(" " + op + " ") + if_proper(body, enclose(body)) + } + + def AND(args: Iterable[Source]): Source = infix("AND", args) + def OR(args: Iterable[Source]): Source = infix("OR", args) + + def and(args: Source*): Source = AND(args) + def or(args: Source*): Source = OR(args) + + val TRUE: Source = "TRUE" + val FALSE: Source = "FALSE" + def member(x: Source, set: Iterable[String]): Source = - if (set.isEmpty) "FALSE" - else set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")") + if (set.isEmpty) FALSE + else OR(set.iterator.map(a => x + " = " + SQL.string(a)).toList) def where_member(x: Source, set: Iterable[String]): Source = " WHERE " + member(x, set) + def where(sql: Source): Source = if_proper(sql, " WHERE " + sql) + + /* types */ @@ -128,7 +145,7 @@ def undefined: String = ident + " IS NULL" def equal(s: String): Source = ident + " = " + string(s) - def where_equal(s: String): Source = "WHERE " + equal(s) + def where_equal(s: String): Source = " WHERE " + equal(s) override def toString: Source = ident } diff -r df17355f1e2c -r 47c2ac81ddd4 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Fri Feb 24 20:52:35 2023 +0100 +++ b/src/Pure/Thy/document_build.scala Sat Feb 25 14:33:19 2023 +0100 @@ -64,8 +64,10 @@ val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) def where_equal(session_name: String, name: String = ""): SQL.Source = - "WHERE " + Data.session_name.equal(session_name) + - (if (name == "") "" else " AND " + Data.name.equal(name)) + SQL.where( + SQL.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 df17355f1e2c -r 47c2ac81ddd4 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Fri Feb 24 20:52:35 2023 +0100 +++ b/src/Pure/Thy/export.scala Sat Feb 25 14:33:19 2023 +0100 @@ -42,9 +42,11 @@ List(session_name, theory_name, name, executable, compressed, body)) def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source = - "WHERE " + Data.session_name.equal(session_name) + - (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) + - (if (name == "") "" else " AND " + Data.name.equal(name)) + 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)))) } def compound_name(a: String, b: String): String = diff -r df17355f1e2c -r 47c2ac81ddd4 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Feb 24 20:52:35 2023 +0100 +++ b/src/Pure/Thy/sessions.scala Sat Feb 25 14:33:19 2023 +0100 @@ -77,8 +77,10 @@ SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body)) def where_equal(session_name: String, name: String = ""): SQL.Source = - "WHERE " + Sources.session_name.equal(session_name) + - (if (name == "") "" else " AND " + Sources.name.equal(name)) + SQL.where( + SQL.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(