* @param end   the end offset, or -1 to go to end of file
     */
    private void copySource(int begin, int end) {
        // Be robust if the analyzer gives us bad offsets.
        try {
            String src = escape((end == -1)
                    ? source.substring(begin)
                    : source.substring(begin, end));
            buffer.append(src);
        } catch (RuntimeException x) {
            // This can happen with files with weird encodings
            // Igore them because of the rareness
        }
        sourceOffset = end;
    }