diff options
| author | Emilio Jesus Gallego Arias | 2018-12-06 04:44:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-09 02:54:02 +0100 |
| commit | d00472c59d15259b486868c5ccdb50b6e602a548 (patch) | |
| tree | 008d862e4308ac8ed94cfbcd94ac26c739b89642 /gramlib | |
| parent | fa20a54d9fbe0f3872614a592fcef7ef56b05e49 (diff) | |
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
Diffstat (limited to 'gramlib')
| -rw-r--r-- | gramlib/ploc.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli index 766e96fdfc..100fbc7271 100644 --- a/gramlib/ploc.mli +++ b/gramlib/ploc.mli @@ -10,6 +10,7 @@ exception Exc of Loc.t * exn for an error. This exception must not be raised by [raise] but rather by [Ploc.raise] (see below), to prevent the risk of several encapsulations of [Ploc.Exc]. *) + val raise : Loc.t -> exn -> 'a (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc], re-raise it (ignoring the new location [loc]), else raise the @@ -29,9 +30,11 @@ val sub : Loc.t -> int -> int -> Loc.t (** [Ploc.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. *) + val after : Loc.t -> int -> int -> Loc.t (** [Ploc.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]. *) + val with_comment : Loc.t -> string -> Loc.t (** Change the comment part of the given location *) |
