# HG changeset patch
# User wenzelm
# Date 1489926887 -3600
# Node ID 2b1cd063e0b25d0d1e071f0e385f319a424aa305
# Parent  52861eebf58d5f3998ce6272618437f81100d96b
proper SQL syntax (according of PostgreSQL);

diff -r 52861eebf58d -r 2b1cd063e0b2 src/Pure/General/sql.scala
--- 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("\"", "\"\""))