diff options
| author | Maxime Dénès | 2016-06-16 02:24:54 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-20 15:05:19 +0200 |
| commit | 058209a96579c73d786a3ceb8a7445cd5b7a8962 (patch) | |
| tree | 26fff33cc21e976a4b82446b7296f74fe730d30f /lib | |
| parent | a8088f565da008d3b1780f38de0ee894e8fd0baa (diff) | |
Add file name, line number and beginning of line position to locations.
Coq locations already had support for this, but were containing dummy
information. We now don't need anymore to reconstruct this information by
browsing the file when printing an error message or enriching exceptions on the
fly.
It also became easier to interface with Coq since locations emitted by the
lexer now always contain full information.
On the API side, Loc.represent disappeared and Loc.t is now exposed as record.
It is less error-prone than manipulating a tuple of 5 integers. Also,
Loc.create takes 5 arguments instead of 3 and a pair.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/loc.ml | 5 | ||||
| -rw-r--r-- | lib/loc.mli | 17 |
2 files changed, 12 insertions, 10 deletions
diff --git a/lib/loc.ml b/lib/loc.ml index afdab928c4..0f9864a9ac 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -8,7 +8,6 @@ (* Locations management *) - type t = { fname : string; (** filename *) line_nb : int; (** start line number *) @@ -19,7 +18,7 @@ type t = { ep : int; (** end position *) } -let create fname line_nb bol_pos (bp, ep) = { +let create fname line_nb bol_pos bp ep = { fname = fname; line_nb = line_nb; bol_pos = bol_pos; line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; } @@ -54,8 +53,6 @@ let merge loc1 loc2 = let unloc loc = (loc.bp, loc.ep) -let represent loc = (loc.fname, loc.line_nb, loc.bol_pos, loc.bp, loc.ep) - let dummy_loc = ghost let join_loc = merge diff --git a/lib/loc.mli b/lib/loc.mli index f39cd2670b..c08e097a87 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -8,7 +8,15 @@ (** {5 Basic types} *) -type t +type t = { + fname : string; (** filename *) + line_nb : int; (** start line number *) + bol_pos : int; (** position of the beginning of start line *) + line_nb_last : int; (** end line number *) + bol_pos_last : int; (** position of the beginning of end line *) + bp : int; (** start position *) + ep : int; (** end position *) +} type 'a located = t * 'a (** Embed a location in a type *) @@ -17,9 +25,9 @@ type 'a located = t * 'a (** This is inherited from CAMPL4/5. *) -val create : string -> int -> int -> (int * int) -> t +val create : string -> int -> int -> int -> int -> t (** Create a location from a filename, a line number, a position of the - beginning of the line and a pair of start and end position *) + beginning of the line, a start and end position *) val unloc : t -> int * int (** Return the start and end position of a location *) @@ -35,9 +43,6 @@ val is_ghost : t -> bool val merge : t -> t -> t -val represent : t -> (string * int * int * int * int) -(** Return the arguments given in [create] *) - (** {5 Located exceptions} *) val add_loc : Exninfo.info -> t -> Exninfo.info |