Excuse me to come back with the issue of character representation. Won't it be acceptable to use a representation with a fixed number of digits? For instance #uXXXX or #uXXXXXX. This eliminates the need for an ending delimiter. I agree that it imposes extra 0 at the beginning of the token but is it really important? -- Manuel