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.ml | |
| parent | a24d1a15858df9574e491bf952a59e700cc75ecc (diff) | |
Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.
Diffstat (limited to 'lib/loc.ml')
| -rw-r--r-- | lib/loc.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/lib/loc.ml b/lib/loc.ml index 09fa45a884..512555b554 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -68,6 +68,10 @@ let merge_opt l1 l2 = match l1, l2 with | None, Some l -> Some l | Some l1, Some l2 -> Some (merge l1 l2) +let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len} + +let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len} + let finer l1 l2 = match l1, l2 with | None, _ -> false | Some l , None -> true @@ -78,6 +82,7 @@ let unloc loc = (loc.bp, loc.ep) let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp } (** Located type *) + type 'a located = t option * 'a let tag ?loc x = loc, x @@ -96,4 +101,3 @@ let raise ?loc e = | Some loc -> let info = Exninfo.add Exninfo.null location loc in Exninfo.iraise (e, info) - |