src/Pure/General/yxml.scala
changeset 34118 ee9f87e11400
parent 34099 2541de190d92
child 34119 ae92efb48784
equal deleted inserted replaced
34117:1eb8d8e3e40a 34118:ee9f87e11400
    58       var code = -1
    58       var code = -1
    59       var rest = 0
    59       var rest = 0
    60       def flush()
    60       def flush()
    61       {
    61       {
    62         if (code != -1) {
    62         if (code != -1) {
    63           if (rest == 0) buf.appendCodePoint(code)
    63           if (rest == 0 && Character.isValidCodePoint(code))
       
    64             buf.appendCodePoint(code)
    64           else buf.append('\uFFFD')
    65           else buf.append('\uFFFD')
    65           code = -1
    66           code = -1
    66           rest = 0
    67           rest = 0
    67         }
    68         }
    68       }
    69       }