src/Pure/General/json.scala
changeset 64761 ae97a5afffcc
parent 64545 25045094d7bb
child 64878 e9208a9301c0
equal deleted inserted replaced
64760:8c1557308eb5 64761:ae97a5afffcc
    30       val result = new StringBuilder
    30       val result = new StringBuilder
    31 
    31 
    32       def string(s: String)
    32       def string(s: String)
    33       {
    33       {
    34         result += '"'
    34         result += '"'
    35         result ++= scala.util.parsing.json.JSONFormat.quoteString(s)
    35         result ++=
       
    36           s.iterator.map {
       
    37             case '"'  => "\\\""
       
    38             case '\\' => "\\\\"
       
    39             case '\b' => "\\b"
       
    40             case '\f' => "\\f"
       
    41             case '\n' => "\\n"
       
    42             case '\r' => "\\r"
       
    43             case '\t' => "\\t"
       
    44             case c =>
       
    45               if (c <= '\u001f' || c >= '\u007f' && c <= '\u009f') "\\u%04x".format(c.toInt)
       
    46               else c
       
    47           }.mkString
    36         result += '"'
    48         result += '"'
    37       }
    49       }
    38 
    50 
    39       def array(list: List[T])
    51       def array(list: List[T])
    40       {
    52       {