# HG changeset patch
# User wenzelm
# Date 1493646146 -7200
# Node ID 366bc4e6a238768d97669f54eb0391a1e0c11b30
# Parent  f1c70c7fea122680c79793da42aadd0eaf5ce5f1
more operations;
tuned;

diff -r f1c70c7fea12 -r 366bc4e6a238 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 01 13:39:27 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 01 15:42:26 2017 +0200
@@ -823,13 +823,13 @@
       val (columns, from) =
         if (ml_statistics) {
           val columns = columns1 ::: List(Build_Info.ml_statistics(table2))
-          val from =
-            "(" + table1.sql + " LEFT JOIN " + table2.sql + " ON " +
+          val join =
+            SQL.join_outer(table1, table2,
               Meta_Info.log_name(table1).sql + " = " +
               Meta_Info.log_name(table2).sql + " AND " +
               Build_Info.session_name(table1).sql + " = " +
-              Build_Info.session_name(table2).sql + ")"
-          (columns, from)
+              Build_Info.session_name(table2).sql)
+          (columns, SQL.enclose(join))
         }
         else (columns1, table1.sql)
 
diff -r f1c70c7fea12 -r 366bc4e6a238 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon May 01 13:39:27 2017 +0200
+++ b/src/Pure/General/sql.scala	Mon May 01 15:42:26 2017 +0200
@@ -37,11 +37,19 @@
     if (Long_Name.is_qualified(s)) s
     else quote(s.replace("\"", "\"\""))
 
+  def enclose(s: String): String = "(" + s + ")"
   def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")
 
   def select(columns: List[Column], distinct: Boolean = false): String =
     "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.sql)) + " FROM "
 
+  def join(table1: Table, table2: Table, sql: String = "", outer: Boolean = false): String =
+    table1.sql + (if (outer) " LEFT OUTER JOIN " else " INNER JOIN ") + table2.sql +
+      (if (sql == "") "" else " ON " + sql)
+
+  def join_outer(table1: Table, table2: Table, sql: String = ""): String =
+    join(table1, table2, sql, outer = true)
+
 
   /* types */