--- a/src/Pure/Admin/build_log.scala Mon Jan 02 15:30:57 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Mon Jan 02 15:41:50 2023 +0100
@@ -772,7 +772,7 @@
SQL.select(columns, distinct = true) +
table1.query_named + SQL.join_outer + aux_table.query_named +
" ON " + version(table1) + " = " + version(aux_table) +
- " ORDER BY " + pull_date(afp)(table1) + " DESC"
+ SQL.order_by(List(pull_date(afp)(table1)), descending = true)
}
--- a/src/Pure/General/sql.scala Mon Jan 02 15:30:57 2023 +0100
+++ b/src/Pure/General/sql.scala Mon Jan 02 15:41:50 2023 +0100
@@ -127,6 +127,9 @@
override def toString: Source = ident
}
+ def order_by(columns: List[Column], descending: Boolean = false): Source =
+ " ORDER BY " + columns.mkString(", ") + (if (descending) " DESC" else "")
+
/* tables */
--- a/src/Pure/Thy/export.scala Mon Jan 02 15:30:57 2023 +0100
+++ b/src/Pure/Thy/export.scala Mon Jan 02 15:41:50 2023 +0100
@@ -88,7 +88,7 @@
def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
val select =
Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) +
- " ORDER BY " + Data.theory_name
+ SQL.order_by(List(Data.theory_name))
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
}
@@ -96,7 +96,7 @@
def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = {
val select =
Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) +
- " ORDER BY " + Data.theory_name + ", " + Data.name
+ SQL.order_by(List(Data.theory_name, Data.name))
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(res =>
Entry_Name(session = session_name,
--- a/src/Pure/Thy/sessions.scala Mon Jan 02 15:30:57 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Jan 02 15:41:50 2023 +0100
@@ -1670,7 +1670,7 @@
): List[Source_File] = {
val select =
Sources.table.select(Nil,
- Sources.where_equal(session_name, name = name) + " ORDER BY " + Sources.name)
+ Sources.where_equal(session_name, name = name) + SQL.order_by(List(Sources.name)))
db.using_statement(select) { stmt =>
(stmt.execute_query().iterator { res =>
val res_name = res.string(Sources.name)