# HG changeset patch
# User wenzelm
# Date 1494252014 -7200
# Node ID 123f2c0995b8de960300191afd51748901a58e8a
# Parent  1001fb86d7f756e49d8caead5f1fe9e8c0fbf167
tuned signature;

diff -r 1001fb86d7f7 -r 123f2c0995b8 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 08 15:13:40 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 08 16:00:14 2017 +0200
@@ -686,6 +686,9 @@
         " GROUP BY " + version)
     }
 
+
+    /* recent pull_date entries */
+
     def recent_time(days: Int): SQL.Source =
       "now() - INTERVAL '" + days.max(0) + " days'"
 
@@ -701,7 +704,7 @@
     {
       val recent = recent_table(days)
       val columns1 = if (pull_date) columns ::: List(Data.pull_date(recent)) else columns
-      table.select(columns1, distinct = distinct) + " INNER JOIN " + recent.query_name +
+      table.select(columns1, distinct = distinct) + SQL.join_inner + recent.query_name +
       " ON " + Prop.isabelle_version(table) + " = " + Prop.isabelle_version(recent)
     }
 
@@ -716,15 +719,15 @@
 
       val aux_columns = log_name :: pull_date :: meta_info_table.columns.tail
       val aux_table = SQL.Table("aux", aux_columns,
-        SQL.select(aux_columns.take(2) ::: aux_columns.drop(2). map(_.apply(table1))) +
-          table1 + " LEFT OUTER JOIN " + table2 + " ON " +
+        SQL.select(aux_columns.take(2) ::: aux_columns.drop(2).map(_.apply(table1))) +
+          table1 + SQL.join_outer + table2 + " ON " +
           Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2))
 
       val columns = aux_columns ::: sessions_table.columns.tail
       SQL.Table("isabelle_build_log", columns,
         {
           SQL.select(log_name(aux_table) :: columns.tail) + aux_table.query_name +
-          " INNER JOIN " + table3 + " ON " + log_name(aux_table) + " = " + log_name(table3)
+          SQL.join_inner + table3 + " ON " + log_name(aux_table) + " = " + log_name(table3)
         })
     }
   }
@@ -977,7 +980,7 @@
         if (ml_statistics) {
           val columns = columns1 ::: List(Data.ml_statistics(table2))
           val join =
-            table1 + " LEFT OUTER JOIN " + table2 + " ON " +
+            table1 + SQL.join_outer + table2 + " ON " +
             Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
             Data.session_name(table1) + " = " + Data.session_name(table2)
           (columns, SQL.enclose(join))
diff -r 1001fb86d7f7 -r 123f2c0995b8 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon May 08 15:13:40 2017 +0200
+++ b/src/Pure/General/sql.scala	Mon May 08 16:00:14 2017 +0200
@@ -48,6 +48,10 @@
     "SELECT " + (if (distinct) "DISTINCT " else "") +
     (if (columns.isEmpty) "*" else commas(columns.map(_.ident))) + " FROM "
 
+  val join_outer: Source = " LEFT OUTER JOIN "
+  val join_inner: Source = " INNER JOIN "
+  def join(outer: Boolean = false): Source = if (outer) join_outer else join_inner
+
 
   /* types */