changeset 65671 | 546020a98a91 |
parent 65669 | d2f19b4a16ae |
child 65672 | 3848e278c278 |
--- a/src/Pure/General/sql.scala Mon May 01 20:14:50 2017 +0200 +++ b/src/Pure/General/sql.scala Mon May 01 20:26:42 2017 +0200 @@ -34,8 +34,7 @@ "'" + s.map(escape_char(_)).mkString + "'" def ident(s: String): String = - if (Long_Name.is_qualified(s)) s - else quote(s.replace("\"", "\"\"")) + Long_Name.implode(Long_Name.explode(s).map(_.replace("\"", "\"\""))) def enclose(s: String): String = "(" + s + ")" def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")