From 52a71bf2b1260ce8f8622878c82caec54d298808 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 5 Apr 2021 16:24:39 +0200 Subject: Locations: Moving functions Ploc.sub and Ploc.after to loc.ml. --- gramlib/ploc.ml | 5 ----- gramlib/ploc.mli | 12 ------------ lib/loc.ml | 6 +++++- lib/loc.mli | 9 +++++++++ 4 files changed, 14 insertions(+), 18 deletions(-) diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml index e121342c94..44ba0c1f44 100644 --- a/gramlib/ploc.ml +++ b/gramlib/ploc.ml @@ -11,8 +11,3 @@ let make_unlined (bp, ep) = let dummy = {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = 0; ep = 0; } - -(* *) - -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} diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli index 4b865110c3..fad883e11a 100644 --- a/gramlib/ploc.mli +++ b/gramlib/ploc.mli @@ -9,15 +9,3 @@ val make_unlined : int * int -> Loc.t val dummy : Loc.t (** [Ploc.dummy] is a dummy location, used in situations when location has no meaning. *) - -(* combining locations *) - -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]. *) 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) - 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 *) -- cgit v1.2.3