aboutsummaryrefslogtreecommitdiff
path: root/gramlib
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-12-06 04:44:27 +0100
committerEmilio Jesus Gallego Arias2018-12-09 02:54:02 +0100
commitd00472c59d15259b486868c5ccdb50b6e602a548 (patch)
tree008d862e4308ac8ed94cfbcd94ac26c739b89642 /gramlib
parentfa20a54d9fbe0f3872614a592fcef7ef56b05e49 (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.mli3
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 *)