aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2021-04-05 16:24:39 +0200
committerHugo Herbelin2021-04-23 15:34:29 +0200
commit52a71bf2b1260ce8f8622878c82caec54d298808 (patch)
tree6a99a52dda6380ccc80166a849a1f489424e29d6
parenta24d1a15858df9574e491bf952a59e700cc75ecc (diff)
Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.
-rw-r--r--gramlib/ploc.ml5
-rw-r--r--gramlib/ploc.mli12
-rw-r--r--lib/loc.ml6
-rw-r--r--lib/loc.mli9
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 *)