# HG changeset patch
# User wenzelm
# Date 1261134652 -3600
# Node ID ee9f87e11400d2cb4ac50a0858a7ffb0c2c2a3f5
# Parent  1eb8d8e3e40a86e817c79adb19eba35849b72473
replace invalid code points -- instead of exception;

diff -r 1eb8d8e3e40a -r ee9f87e11400 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Fri Dec 18 11:44:25 2009 +0100
+++ b/src/Pure/General/yxml.scala	Fri Dec 18 12:10:52 2009 +0100
@@ -60,7 +60,8 @@
       def flush()
       {
         if (code != -1) {
-          if (rest == 0) buf.appendCodePoint(code)
+          if (rest == 0 && Character.isValidCodePoint(code))
+            buf.appendCodePoint(code)
           else buf.append('\uFFFD')
           code = -1
           rest = 0