package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a
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.