| author | wenzelm |
| Sun Sep 04 15:44:20 2016 +0200 (2016-09-04) | |
| changeset 63778 | e06e899b78d0 |
| child 63779 | 9da65bc75610 |
| permissions | -rw-r--r-- |
| 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 |
} |