author | wenzelm |
Mon, 01 May 2017 20:26:42 +0200 | |
changeset 65671 | 546020a98a91 |
parent 65670 | 490649872acc |
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("(", ", ", ")")