		Search-engine friendly clone of the ACL2 documentation.

Pproc-*-group-part

Preprocess zero or more group parts.

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).

According to the grammar, a preprocessing-file consists of zero or more group-parts. Each group part ends with a new line, and non-empty files must end with new line [C17:5.1.1.2/1, phase 4]. Thus, we can detect whether there is a group part or not by checking for end of file (this may need to be relaxed at some point, since GCC is more lenient on this front).