From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- lib/cErrors.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'lib/cErrors.ml') diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 830a9e3ce..38ed3f5ba 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -33,12 +33,12 @@ let is_anomaly = function | Anomaly _ -> true | _ -> false -exception UserError of string * std_ppcmds (* User errors *) +exception UserError of string option * std_ppcmds (* User errors *) let todo s = prerr_string ("TODO: "^s^"\n") -let user_err ?loc s strm = Loc.raise ?loc (UserError (s,strm)) -let error string = user_err "_" (str string) +let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) +let error string = user_err (str string) let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) @@ -112,7 +112,7 @@ let iprint_no_report (e, info) = let _ = register_handler begin function | UserError(s, pps) -> - hov 0 (str "Error: " ++ where (Some s) ++ pps) + hov 0 (str "Error: " ++ where s ++ pps) | _ -> raise Unhandled end -- cgit v1.2.3