package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704
doc/lambdapi.common/Common/Pos/index.html
Module Common.PosSource
Positions in Lambdapi files.
type pos = {fname : string option;(*File name for the position.
*)start_line : int;(*Line number of the starting point.
*)start_col : int;(*Column number (utf8) of the starting point.
*)end_line : int;(*Line number of the ending point.
*)end_col : int;(*Column number (utf8) of the ending point.
*)
}Type of a position, corresponding to a continuous range of characters in a (utf8-encoded) source.
Total comparison function on pos.
type 'a loc = {elt : 'a;(*The element that is being localised.
*)pos : popt;(*Position of the element in the source code.
*)
}Type constructor extending a type (e.g. a piece of abstract syntax) with a a source code position.
none elt wraps elt in a 'a loc structure without any specific source code position.
to_string ?print_fname pos transforms pos into a readable string. If print_fname is true (the default), the filename contained in pos is printed.
pp ppf pos prints the optional position pos on ppf.
short ppf pos prints the optional position pos on ppf.
map f loc applies function f on the value of loc and keeps the position unchanged.
locate ?fname loc converts the pair of position loc and filename fname of the Lexing library into a pos.
make_pos lps elt creates a located element from the lexing positions lps and the element elt.
val print_file_contents :
escape:(string -> string) ->
delimiters:(string * string) ->
popt Lplib.Base.ppprint_file_contents escape sep delimiters pos prints the contents of the file at position pos. sep is the separator replacing each newline (e.g. "<br>\n"). delimiters is a pair of delimiters used to wrap the "unknown location" message returned when the position does not refer to a file. escape is used to escape the file contents.