# HG changeset patch # User wenzelm # Date 1493566334 -7200 # Node ID 69dfec14b0dff4e889aa62641df1cd01e31a2cb7 # Parent 7cf60e2b9115a07bfeb45fdc1d9ee3b553570471 tuned signature; diff -r 7cf60e2b9115 -r 69dfec14b0df src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Sun Apr 30 17:02:56 2017 +0200 +++ b/src/Pure/Admin/build_log.scala Sun Apr 30 17:32:14 2017 +0200 @@ -812,8 +812,7 @@ if (session_names.isEmpty) where_log_name else where_log_name + " AND " + - session_names.map(a => - Build_Info.session_name(table1).sql_name + " = " + SQL.quote_string(a)). + session_names.map(a => Build_Info.session_name(table1).sql_name + " = " + SQL.string(a)). mkString("(", " OR ", ")") val columns1 = table1.columns.tail.map(_.apply(table1)) @@ -822,8 +821,8 @@ val columns = columns1 ::: List(Build_Info.ml_statistics(table2)) val from = "(" + - SQL.quote_ident(table1.name) + " LEFT JOIN " + - SQL.quote_ident(table2.name) + " ON " + + SQL.ident(table1.name) + " LEFT JOIN " + + SQL.ident(table2.name) + " ON " + Meta_Info.log_name(table1).sql_name + " = " + Meta_Info.log_name(table2).sql_name + " AND " + Build_Info.session_name(table1).sql_name + " = " + @@ -831,7 +830,7 @@ ")" (columns, from) } - else (columns1, SQL.quote_ident(table1.name)) + else (columns1, SQL.ident(table1.name)) val sessions = using(db.statement(SQL.select(columns) + from + " " + where))(stmt => diff -r 7cf60e2b9115 -r 69dfec14b0df src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Sun Apr 30 17:02:56 2017 +0200 +++ b/src/Pure/General/sql.scala Sun Apr 30 17:32:14 2017 +0200 @@ -30,10 +30,10 @@ case _ => c.toString } - def quote_string(s: String): String = + def string(s: String): String = "'" + s.map(escape_char(_)).mkString + "'" - def quote_ident(s: String): String = + def ident(s: String): String = if (Long_Name.is_qualified(s)) s else quote(s.replace("\"", "\"\"")) @@ -94,12 +94,12 @@ def apply(table: Table): Column = Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key) - def sql_name: String = quote_ident(name) + def sql_name: String = ident(name) def sql_decl(sql_type: Type.Value => String): String = sql_name + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "") def sql_where_eq: String = "WHERE " + sql_name + " = " - def sql_where_equal(s: String): String = sql_where_eq + quote_string(s) + def sql_where_equal(s: String): String = sql_where_eq + string(s) override def toString: String = sql_decl(sql_type_default) } @@ -129,32 +129,32 @@ def sql_create(strict: Boolean, sql_type: Type.Value => String): String = "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") + - quote_ident(name) + " " + sql_columns(sql_type) + ident(name) + " " + sql_columns(sql_type) def sql_drop(strict: Boolean): String = - "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name) + "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + ident(name) 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 ") + quote_ident(index_name) + " ON " + - quote_ident(name) + " " + enclosure(index_columns.map(_.name)) + (if (strict) "" else "IF NOT EXISTS ") + ident(index_name) + " ON " + + ident(name) + " " + enclosure(index_columns.map(_.name)) def sql_drop_index(index_name: String, strict: Boolean): String = - "DROP INDEX " + (if (strict) "" else "IF EXISTS ") + quote_ident(index_name) + "DROP INDEX " + (if (strict) "" else "IF EXISTS ") + ident(index_name) def sql_insert: String = - "INSERT INTO " + quote_ident(name) + " VALUES " + enclosure(columns.map(_ => "?")) + "INSERT INTO " + ident(name) + " VALUES " + enclosure(columns.map(_ => "?")) def sql_delete: String = - "DELETE FROM " + quote_ident(name) + "DELETE FROM " + ident(name) def sql_select(select_columns: List[Column], distinct: Boolean = false): String = - select(select_columns, distinct = distinct) + quote_ident(name) + select(select_columns, distinct = distinct) + ident(name) override def toString: String = - "TABLE " + quote_ident(name) + " " + sql_columns(sql_type_default) + "TABLE " + ident(name) + " " + sql_columns(sql_type_default) }