proper quote (amending 546020a98a91): e.g. relevant for "ISABELLE_BUILD_OPTIONS";
authorwenzelm
Tue, 02 May 2017 10:25:27 +0200
changeset 65677 7d25b8dbdbfa
parent 65676 c9c352583b16
child 65678 aaba2e0c247c
child 65680 378a2f11bec9
proper quote (amending 546020a98a91): e.g. relevant for "ISABELLE_BUILD_OPTIONS";
src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue May 02 10:12:26 2017 +0200
+++ b/src/Pure/General/sql.scala	Tue May 02 10:25:27 2017 +0200
@@ -34,7 +34,7 @@
     "'" + s.map(escape_char(_)).mkString + "'"
 
   def identifer(s: String): String =
-    Long_Name.implode(Long_Name.explode(s).map(_.replace("\"", "\"\"")))
+    Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))
 
   def enclose(s: String): String = "(" + s + ")"
   def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")