# HG changeset patch
# User wenzelm
# Date 1672670510 -3600
# Node ID c6cdf2a641f4b51d196918b5e985975269a2c0f4
# Parent  9ed58e165110f9122ed5cf2887873b4583785d9e
clarified signature: more explicit types;

diff -r 9ed58e165110 -r c6cdf2a641f4 src/Pure/Admin/build_log.scala
--- 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)
     }
 
 
diff -r 9ed58e165110 -r c6cdf2a641f4 src/Pure/General/sql.scala
--- 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 */
 
diff -r 9ed58e165110 -r c6cdf2a641f4 src/Pure/Thy/export.scala
--- 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,
diff -r 9ed58e165110 -r c6cdf2a641f4 src/Pure/Thy/sessions.scala
--- 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)