		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 newline, skipping over whitespace and comments. If we find no token or newline, it is an error, because it means that the file has some whitespace or comments without a terminating newline; this function is called (by pproc-*-group-part) only if we are not at the end of file.

If we find a newline, 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.

If we find a hash, we have a directive; otherwise, we have a text line with tokens.