A solution might be that the GWT editor outputs {{xhtml}}character{{/
xhtml}}
This should always work.
WDYT?
-Vincent
On Sep 24, 2008, at 2:31 PM, Vincent Massol wrote:
  Hi,
 We have a problem with the GWT character map. It contains some
 characters that are not ISO-8859-1. The problem is that since our
 default encoding is ISO-8859-1 (<?xml version="1.0"
 encoding="ISO-8859-1" ?>) the browser replaces for example this
 character   ∞ with ∞
 Our rendering doesn't accept HTML so this value is escaped and is
 shown as is.
 So we have several non-satisfactory options:
 1) Switch to UTF8 by default. A good thing but that won't solve the
 problem for those using the GWT editor in ISO-8859-1 encoding.
 2) Modify the GWT editor character map so that it only shows
 characters valid with the current encoding. This is a pity since it
 should be possible to display other chars since the browser knows how
 to display them even though the user is not in the correct encoding
 3) Introduce a wiki syntax for representing characters not allowed in
 the current encoding. However this means we'll still need to replace
 ∞ with this syntax before the rendering is called and this
 forbids users to enter ∞ in the wiki editor so this is not good.
 Any better idea?
 WDYT?
 Thanks
 -Vincent