diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 5 | ||||
| -rw-r--r-- | lib/util.mli | 6 |
2 files changed, 11 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index d80f09062..56d6717e3 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -31,6 +31,11 @@ let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm)) let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) let join_loc (deb1,_) (_,fin2) = (deb1,fin2) +(* Like Exc_located, but specifies the outermost file read, the filename + associated to the location of the error, and the error itself. *) + +exception Error_in_file of string * (bool * string * Util.loc) * exn + (* Projections from triplets *) let pi1 (a,_,_) = a diff --git a/lib/util.mli b/lib/util.mli index 58d5150b7..e4a2ef707 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -41,6 +41,12 @@ val user_err_loc : loc * string * std_ppcmds -> 'a val invalid_arg_loc : loc * string -> 'a val join_loc : loc -> loc -> loc +(* Like [Exc_located], but specifies the outermost file read, the + input buffer associated to the location of the error (or the module name + if boolean is true), and the error itself. *) + +exception Error_in_file of string * (bool * string * loc) * exn + (*s Projections from triplets *) val pi1 : 'a * 'b * 'c -> 'a |