clarified signature: more explicit types;

--- 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)