String documentation() {
        if (documentation != null)
            return documentation;
        if (docPath != null) {
            // read from file
            try {
                InputStream s = docPath.openInputStream();
                documentation = readHTMLDocumentation(s, docPath);
            } catch (IOException exc) {
                documentation = "";
                env.error(null, "javadoc.File_Read_Error", docPath.getName());
            }
        } else {
            // no doc file to be had
            documentation = "";
        }
        return documentation;
    }