more operations;
authorwenzelm
Mon May 01 15:42:26 2017 +0200 (2017-05-01)
changeset 65668366bc4e6a238
parent 65667 f1c70c7fea12
child 65669 d2f19b4a16ae
more operations;
tuned;
src/Pure/Admin/build_log.scala
src/Pure/General/sql.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Mon May 01 13:39:27 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Mon May 01 15:42:26 2017 +0200
     1.3 @@ -823,13 +823,13 @@
     1.4        val (columns, from) =
     1.5          if (ml_statistics) {
     1.6            val columns = columns1 ::: List(Build_Info.ml_statistics(table2))
     1.7 -          val from =
     1.8 -            "(" + table1.sql + " LEFT JOIN " + table2.sql + " ON " +
     1.9 +          val join =
    1.10 +            SQL.join_outer(table1, table2,
    1.11                Meta_Info.log_name(table1).sql + " = " +
    1.12                Meta_Info.log_name(table2).sql + " AND " +
    1.13                Build_Info.session_name(table1).sql + " = " +
    1.14 -              Build_Info.session_name(table2).sql + ")"
    1.15 -          (columns, from)
    1.16 +              Build_Info.session_name(table2).sql)
    1.17 +          (columns, SQL.enclose(join))
    1.18          }
    1.19          else (columns1, table1.sql)
    1.20  
     2.1 --- a/src/Pure/General/sql.scala	Mon May 01 13:39:27 2017 +0200
     2.2 +++ b/src/Pure/General/sql.scala	Mon May 01 15:42:26 2017 +0200
     2.3 @@ -37,11 +37,19 @@
     2.4      if (Long_Name.is_qualified(s)) s
     2.5      else quote(s.replace("\"", "\"\""))
     2.6  
     2.7 +  def enclose(s: String): String = "(" + s + ")"
     2.8    def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")
     2.9  
    2.10    def select(columns: List[Column], distinct: Boolean = false): String =
    2.11      "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.sql)) + " FROM "
    2.12  
    2.13 +  def join(table1: Table, table2: Table, sql: String = "", outer: Boolean = false): String =
    2.14 +    table1.sql + (if (outer) " LEFT OUTER JOIN " else " INNER JOIN ") + table2.sql +
    2.15 +      (if (sql == "") "" else " ON " + sql)
    2.16 +
    2.17 +  def join_outer(table1: Table, table2: Table, sql: String = ""): String =
    2.18 +    join(table1, table2, sql, outer = true)
    2.19 +
    2.20  
    2.21    /* types */
    2.22