		Search-engine friendly clone of the ACL2 documentation.

Extended-characters

Vl-location

Representation of a point in a source file.

This is a product type introduced by defprod.

Fields

filename — stringp
line — posp
col — natp

Each vl-location-p represents some location in a source code file. These locations are attached to characters and module items to provide context during error reporting.

Subtopics

Vl-location-p: Recognizer for vl-location structures.
Vl-location-fix: Fixing function for vl-location structures.
Vl-string-between-locs: Given a string, extract all text that occurs between two vl-location-ps.
Vl-location-between-p: (vl-location-between-p x min max) is true exactly when x is in the same file as min and max, and inclusively falls between these bounds.
Vl-string-findloc: Traverse a string to determine the position of a vl-location-p.
Vl-location-equiv: Basic equivalence relation for vl-location structures.
Make-vl-location: Basic constructor macro for vl-location structures.
Vl-location-string: Convert an vl-location-p into a string.
Vl-location->filename: Get the filename field from a vl-location.
Vl-location->line: Get the line field from a vl-location.
Change-vl-location: Modifying constructor for vl-location structures.
Vl-location->col: Get the col field from a vl-location.
*vl-fakeloc*: A "fake" vl-location-p which we use when generating our own extended-characters and module items.