# HG changeset patch # User wenzelm # Date 1493817022 -7200 # Node ID 4edac706bc5efcdde8c4ef3971fd1f4caae942bf # Parent b82f2990161a7d3bc3457947008e98f27d120cf1 tuned signature; diff -r b82f2990161a -r 4edac706bc5e src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Wed May 03 14:55:34 2017 +0200 +++ b/src/Pure/Admin/build_log.scala Wed May 03 15:10:22 2017 +0200 @@ -684,7 +684,7 @@ val table1 = meta_info_table val table2 = sessions_table SQL.select(log_name(table1) :: columns.tail) + - SQL.join(table1, table2, log_name(table1).sql + " = " + log_name(table2).sql) + SQL.join(table1, table2, log_name(table1).ident + " = " + log_name(table2).ident) }) } @@ -696,22 +696,22 @@ def pull_date_table(name: String, version: SQL.Column): SQL.Table = SQL.Table("isabelle_build_log_" + name, List(version.copy(primary_key = true), pull_date), view = // PostgreSQL - "SELECT " + version.sql + ", min(" + Prop.build_start.sql + ") AS " + pull_date.sql + - " FROM " + meta_info_table.sql + - " WHERE " + version.sql + " IS NOT NULL AND" + Prop.build_start.sql + " IS NOT NULL" + - " GROUP BY " + version.sql) + "SELECT " + version.ident + ", min(" + Prop.build_start.ident + ") AS " + pull_date.ident + + " FROM " + meta_info_table.ident + + " WHERE " + version.ident + " IS NOT NULL AND" + Prop.build_start.ident + " IS NOT NULL" + + " GROUP BY " + version.ident) val isabelle_pull_date_table = pull_date_table("isabelle_pull_date", Prop.isabelle_version) val afp_pull_date_table = pull_date_table("afp_pull_date", Prop.afp_version) def recent(table: SQL.Table, days: Int): String = table.sql_select(table.columns) + - " WHERE " + pull_date(table).sql + " > now() - INTERVAL '" + days.max(0) + " days'" + " WHERE " + pull_date(table).ident + " > now() - INTERVAL '" + days.max(0) + " days'" def select_recent(table: SQL.Table, columns: List[SQL.Column], days: Int): String = table.sql_select(columns) + " INNER JOIN (" + recent(isabelle_pull_date_table, days) + ") AS recent" + - " ON " + Prop.isabelle_version(table).sql + " = recent." + Prop.isabelle_version.sql + " ON " + Prop.isabelle_version(table).ident + " = recent." + Prop.isabelle_version.ident } @@ -927,12 +927,12 @@ val where_log_name = Data.log_name(table1).sql_where_equal(log_name) + " AND " + - Data.session_name(table1).sql + " <> ''" + Data.session_name(table1).ident + " <> ''" val where = if (session_names.isEmpty) where_log_name else where_log_name + " AND " + - session_names.map(a => Data.session_name(table1).sql + " = " + SQL.string(a)). + session_names.map(a => Data.session_name(table1).ident + " = " + SQL.string(a)). mkString("(", " OR ", ")") val columns1 = table1.columns.tail.map(_.apply(table1)) @@ -941,13 +941,13 @@ val columns = columns1 ::: List(Data.ml_statistics(table2)) val join = SQL.join_outer(table1, table2, - Data.log_name(table1).sql + " = " + - Data.log_name(table2).sql + " AND " + - Data.session_name(table1).sql + " = " + - Data.session_name(table2).sql) + Data.log_name(table1).ident + " = " + + Data.log_name(table2).ident + " AND " + + Data.session_name(table1).ident + " = " + + Data.session_name(table2).ident) (columns, SQL.enclose(join)) } - else (columns1, table1.sql) + else (columns1, table1.ident) val sessions = using(db.statement(SQL.select(columns) + from + " " + where))(stmt => diff -r b82f2990161a -r 4edac706bc5e src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Wed May 03 14:55:34 2017 +0200 +++ b/src/Pure/General/sql.scala Wed May 03 15:10:22 2017 +0200 @@ -33,17 +33,17 @@ def string(s: String): String = "'" + s.map(escape_char(_)).mkString + "'" - def identifer(s: String): String = + def ident(s: String): String = Long_Name.implode(Long_Name.explode(s).map(a => quote(a.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 " + "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.ident)) + " 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 + + table1.ident + (if (outer) " LEFT OUTER JOIN " else " INNER JOIN ") + table2.ident + (if (sql == "") "" else " ON " + sql) def join_outer(table1: Table, table2: Table, sql: String = ""): String = @@ -101,11 +101,12 @@ def apply(table: Table): Column = Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key) - def sql: String = identifer(name) + def ident: String = SQL.ident(name) + def sql_decl(sql_type: Type.Value => String): String = - identifer(name) + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "") + ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "") - def sql_where_eq: String = "WHERE " + identifer(name) + " = " + def sql_where_eq: String = "WHERE " + ident + " = " def sql_where_equal(s: String): String = sql_where_eq + string(s) override def toString: String = sql_decl(sql_type_default) @@ -126,7 +127,7 @@ def is_view: Boolean = view != "" - def sql: String = identifer(name) + def ident: String = SQL.ident(name) def sql_columns(sql_type: Type.Value => String): String = { @@ -140,26 +141,24 @@ def sql_create(strict: Boolean, sql_type: Type.Value => String): String = "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") + - identifer(name) + " " + sql_columns(sql_type) + ident + " " + sql_columns(sql_type) def sql_create_index( index_name: String, index_columns: List[Column], strict: Boolean, unique: Boolean): String = "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " + - (if (strict) "" else "IF NOT EXISTS ") + identifer(index_name) + " ON " + - identifer(name) + " " + enclosure(index_columns.map(_.name)) + (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " + + ident + " " + enclosure(index_columns.map(_.name)) - def sql_insert: String = - "INSERT INTO " + identifer(name) + " VALUES " + enclosure(columns.map(_ => "?")) + def sql_insert: String = "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) - def sql_delete: String = - "DELETE FROM " + identifer(name) + def sql_delete: String = "DELETE FROM " + ident def sql_select(select_columns: List[Column], distinct: Boolean = false): String = - select(select_columns, distinct = distinct) + identifer(name) + select(select_columns, distinct = distinct) + ident override def toString: String = - "TABLE " + identifer(name) + " " + sql_columns(sql_type_default) + "TABLE " + ident + " " + sql_columns(sql_type_default) } @@ -308,7 +307,7 @@ { require(table.is_view) if (strict || !tables.contains(table.name)) { - val sql = "CREATE VIEW " + identifer(table.name) + " AS " + table.view + val sql = "CREATE VIEW " + ident(table.name) + " AS " + table.view using(statement(sql))(_.execute()) } }