package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
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