equal
deleted
inserted
replaced
32 |
32 |
33 def string(s: String): String = |
33 def string(s: String): String = |
34 "'" + s.map(escape_char(_)).mkString + "'" |
34 "'" + s.map(escape_char(_)).mkString + "'" |
35 |
35 |
36 def ident(s: String): String = |
36 def ident(s: String): String = |
37 if (Long_Name.is_qualified(s)) s |
37 Long_Name.implode(Long_Name.explode(s).map(_.replace("\"", "\"\""))) |
38 else quote(s.replace("\"", "\"\"")) |
|
39 |
38 |
40 def enclose(s: String): String = "(" + s + ")" |
39 def enclose(s: String): String = "(" + s + ")" |
41 def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")") |
40 def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")") |
42 |
41 |
43 def select(columns: List[Column], distinct: Boolean = false): String = |
42 def select(columns: List[Column], distinct: Boolean = false): String = |