diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-16 02:24:54 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-20 15:05:19 +0200 |
| commit | 058209a96579c73d786a3ceb8a7445cd5b7a8962 (patch) | |
| tree | 26fff33cc21e976a4b82446b7296f74fe730d30f /parsing/cLexer.mli | |
| 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 'parsing/cLexer.mli')
| -rw-r--r-- | parsing/cLexer.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 24b0ec847..d99ba3557 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -17,6 +17,9 @@ type location_table val location_table : unit -> location_table val restore_location_table : location_table -> unit +(** [set_current_file fname] sets the filename in locations emitted by the lexer *) +val set_current_file : fname:string -> unit + val check_ident : string -> unit val is_ident : string -> bool val check_keyword : string -> unit |