src/Pure/Tools/sql.scala
author wenzelm
Sun Sep 04 15:44:20 2016 +0200 (2016-09-04)
changeset 63778 e06e899b78d0
child 63779 9da65bc75610
permissions -rw-r--r--
clarified modules;
tuned signature;
wenzelm@63778
     1
/*  Title:      Pure/Tools/sql.scala
wenzelm@63778
     2
    Author:     Makarius
wenzelm@63778
     3
wenzelm@63778
     4
Support for SQL.
wenzelm@63778
     5
*/
wenzelm@63778
     6
wenzelm@63778
     7
package isabelle
wenzelm@63778
     8
wenzelm@63778
     9
wenzelm@63778
    10
object SQL
wenzelm@63778
    11
{
wenzelm@63778
    12
  /* concrete syntax */
wenzelm@63778
    13
wenzelm@63778
    14
  def quote_char(c: Char): String =
wenzelm@63778
    15
    c match {
wenzelm@63778
    16
      case '\u0000' => "\\0"
wenzelm@63778
    17
      case '\'' => "\\'"
wenzelm@63778
    18
      case '\"' => "\\\""
wenzelm@63778
    19
      case '\b' => "\\b"
wenzelm@63778
    20
      case '\n' => "\\n"
wenzelm@63778
    21
      case '\r' => "\\r"
wenzelm@63778
    22
      case '\t' => "\\t"
wenzelm@63778
    23
      case '\u001a' => "\\Z"
wenzelm@63778
    24
      case '\\' => "\\\\"
wenzelm@63778
    25
      case _ => c.toString
wenzelm@63778
    26
    }
wenzelm@63778
    27
wenzelm@63778
    28
  def quote_string(s: String): String =
wenzelm@63778
    29
    quote(s.map(quote_char(_)).mkString)
wenzelm@63778
    30
wenzelm@63778
    31
  def quote_ident(s: String): String = "`" + s + "`"
wenzelm@63778
    32
}