aboutsummaryrefslogtreecommitdiff
path: root/lib/loc.mli
diff options
context:
space:
mode:
authorHugo Herbelin2021-04-05 16:24:39 +0200
committerHugo Herbelin2021-04-23 15:34:29 +0200
commit52a71bf2b1260ce8f8622878c82caec54d298808 (patch)
tree6a99a52dda6380ccc80166a849a1f489424e29d6 /lib/loc.mli
parenta24d1a15858df9574e491bf952a59e700cc75ecc (diff)
Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.
Diffstat (limited to 'lib/loc.mli')
-rw-r--r--lib/loc.mli9
1 files changed, 9 insertions, 0 deletions
diff --git a/lib/loc.mli b/lib/loc.mli
index c54a837bb4..2bbfaa5cce 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -45,6 +45,15 @@ val merge : t -> t -> t
val merge_opt : t option -> t option -> t option
(** Merge locations, usually generating the largest possible span *)
+val sub : t -> int -> int -> t
+(** [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 : t -> int -> int -> t
+(** [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 finer : t option -> t option -> bool
(** Answers [true] when the first location is more defined, or, when
both defined, included in the second one *)