		Search-engine friendly clone of the ACL2 documentation.

Pproc-text-line

Preprocess a (non-empty) text line.

Signature
(pproc-text-line nontoknls path file preprocessed preprocessing rev-lexemes ppstate state) → (mv erp new-rev-lexemes new-ppstate new-preprocessed state)
Arguments: nontoknls — Guard (plexeme-listp nontoknls).; 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).

That is, preprocess a line that does not start with a hash (possibly after some white space and comments). This is called after putting back the first token of the line, but without having put back any leading white space or comments, since those do not matter for the purpose of preprocessing the text line. Recall that empty text lines, i.e. with no tokens (but possibly with some white space and comments), are already handlede in pproc-group-part.