--- a/src/Pure/General/sql.scala Sun Mar 19 13:05:06 2017 +0100
+++ b/src/Pure/General/sql.scala Sun Mar 19 13:34:47 2017 +0100
@@ -16,7 +16,7 @@
/* concrete syntax */
- def quote_char(c: Char): String =
+ def escape_char(c: Char): String =
c match {
case '\u0000' => "\\0"
case '\'' => "\\'"
@@ -31,7 +31,7 @@
}
def quote_string(s: String): String =
- quote(s.map(quote_char(_)).mkString)
+ "'" + s.map(escape_char(_)).mkString + "'"
def quote_ident(s: String): String =
quote(s.replace("\"", "\"\""))