src/Pure/Tools/sql.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/sql.scala	Sun Sep 04 15:44:20 2016 +0200
@@ -0,0 +1,32 @@
+/*  Title:      Pure/Tools/sql.scala
+    Author:     Makarius
+
+Support for SQL.
+*/
+
+package isabelle
+
+
+object SQL
+{
+  /* concrete syntax */
+
+  def quote_char(c: Char): String =
+    c match {
+      case '\u0000' => "\\0"
+      case '\'' => "\\'"
+      case '\"' => "\\\""
+      case '\b' => "\\b"
+      case '\n' => "\\n"
+      case '\r' => "\\r"
+      case '\t' => "\\t"
+      case '\u001a' => "\\Z"
+      case '\\' => "\\\\"
+      case _ => c.toString
+    }
+
+  def quote_string(s: String): String =
+    quote(s.map(quote_char(_)).mkString)
+
+  def quote_ident(s: String): String = "`" + s + "`"
+}