diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-06 11:41:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-14 13:31:27 +0200 |
| commit | 7f816f00fed5ee7c7e94bd5f02a88880cdfa96aa (patch) | |
| tree | 3c0d25c6cb26b5425ec5bc38ed9707c87a8d7e52 /lib/loc.mli | |
| parent | a86bdf0cae05e46d5f0516f29254aeb72bf08de7 (diff) | |
Using an algebraic type for distinguishing toplevel input from location in file.
Diffstat (limited to 'lib/loc.mli')
| -rw-r--r-- | lib/loc.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/lib/loc.mli b/lib/loc.mli index 1fbaae836..d4061e044 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -8,8 +8,12 @@ (** {5 Basic types} *) +type source = + | InFile of string + | ToplevelInput + type t = { - fname : string; (** filename *) + fname : source; (** filename or toplevel input *) line_nb : int; (** start line number *) bol_pos : int; (** position of the beginning of start line *) line_nb_last : int; (** end line number *) @@ -22,7 +26,7 @@ type t = { (** This is inherited from CAMPL4/5. *) -val create : string -> int -> int -> int -> int -> t +val create : source -> int -> int -> int -> int -> t (** Create a location from a filename, a line number, a position of the beginning of the line, a start and end position *) |