diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 23:40:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:00:43 +0200 |
| commit | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (patch) | |
| tree | 70dd074f483c34e9f71da20edf878062a4b5b3af /lib/loc.ml | |
| parent | 84eb5cd72a015c45337a5a6070c5651f56be6e74 (diff) | |
[location] Remove Loc.ghost.
Now it is a private field, locations are optional.
Diffstat (limited to 'lib/loc.ml')
| -rw-r--r-- | lib/loc.ml | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/lib/loc.ml b/lib/loc.ml index 2a785fac4..3051ca7b9 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -26,12 +26,6 @@ let make_loc (bp, ep) = { fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = bp; ep = ep; } -let ghost = { - fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; - bp = 0; ep = 0; } - -let is_ghost loc = loc.ep = 0 - let merge loc1 loc2 = if loc1.bp < loc2.bp then if loc1.ep < loc2.ep then { @@ -51,15 +45,24 @@ let merge loc1 loc2 = bp = loc2.bp; ep = loc1.ep; } else loc2 +let merge_opt l1 l2 = Option.cata (fun l1 -> merge l1 l2) l2 l1 +let opt_merge l1 l2 = Option.cata (fun l2 -> merge l1 l2) l1 l2 + let unloc loc = (loc.bp, loc.ep) -let dummy_loc = ghost let join_loc = merge (** Located type *) type 'a located = t * 'a +let is_ghost loc = loc.ep = 0 + +let ghost = { + fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; + bp = 0; ep = 0; } + +let internal_ghost = ghost let to_pair x = x let tag ?loc x = Option.default ghost loc, x let obj (_,x) = x |