package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.lib/Loc/index.html
Module Loc
Source
Basic types
type t = {
fname : source;
(*filename or toplevel input
*)line_nb : int;
(*start line number
*)bol_pos : int;
(*position of the beginning of start line
*)line_nb_last : int;
(*end line number
*)bol_pos_last : int;
(*position of the beginning of end line
*)bp : int;
(*start position
*)ep : int;
(*end position
*)
}
Location manipulation
This is inherited from CAMPL4/5.
Create a location from a filename, a line number, a position of the beginning of the line, a start and end position
Merge locations, usually generating the largest possible span
sub loc sh len
is the location loc
shifted with sh
characters and with length len
. The previous ending position of the location is lost.
after loc sh len
is the location just after loc (starting at the end position of loc
) shifted with sh
characters and of length len
.
Answers true
when the first location is more defined, or, when both defined, included in the second one
shift_loc loc n p
shifts the beginning of location by n
and the end by p
; it is assumed that the shifts do not change the lines at which the location starts and ends
Located exceptions
Adding location to an exception
Retrieving the optional location of an exception