diff options
| author | Hugo Herbelin | 2021-04-05 16:24:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2021-04-23 15:34:29 +0200 |
| commit | 52a71bf2b1260ce8f8622878c82caec54d298808 (patch) | |
| tree | 6a99a52dda6380ccc80166a849a1f489424e29d6 /lib/loc.mli | |
| parent | a24d1a15858df9574e491bf952a59e700cc75ecc (diff) | |
Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.
Diffstat (limited to 'lib/loc.mli')
| -rw-r--r-- | lib/loc.mli | 9 |
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 *) |
