		Search-engine friendly clone of the ACL2 documentation.

Pproc-group-part

Preprocess a group part.

Signature
(pproc-group-part path file preprocessed preprocessing rev-lexemes ppstate state) → (mv erp new-rev-lexemes new-ppstate new-preprocessed state)
Arguments: path — Guard (stringp path).; file — Guard (stringp file).; preprocessed — Guard (string-plexeme-list-alistp preprocessed).; preprocessing — Guard (string-listp preprocessing).; rev-lexemes — Guard (plexeme-listp rev-lexemes).; ppstate — Guard (ppstatep ppstate).
Returns: new-rev-lexemes — Type (plexeme-listp new-rev-lexemes).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).; new-preprocessed — Type (string-plexeme-list-alistp new-preprocessed).

We read the next token or new line, skipping over white space and comments. If we find no token or new line, it is an error, because it means that the file has some white space or comments without a terminating new line; this function is called (by pproc-*-group-part) only if we are not at the end of file.

If we find a new line, it means that we have a text line (see grammar) without tokens. In this case we have finished the group part and we return all the lexemes. For example, this could contain comments, which we therefore preserve.

If we find a hash, we have a directive, which we handle in a separate function. We discard any white space and comments preceding the hash.

If we do not find a hash, we have a text line with tokens: we put back the token and we call a separate function. We pass any preceding white space and comments to that function.