diff options
Diffstat (limited to 'lib/cErrors.ml')
| -rw-r--r-- | lib/cErrors.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 323dc8c1a4..a23cf3aaf1 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -79,7 +79,7 @@ let is_anomaly = function (** Printing of additional error info, from Exninfo *) let additional_error_info_handler = ref [] -let register_additional_error_info (f : Exninfo.info -> (Pp.t option Loc.located) option) = +let register_additional_error_info (f : Exninfo.info -> (Pp.t Loc.located) option) = additional_error_info_handler := f :: !additional_error_info_handler (** [print_gen] is a general exception printer which tries successively @@ -93,18 +93,15 @@ let rec print_gen ~anomaly ~extra_msg stk e = | h::stk' -> match h e with | Some err_msg -> - Option.cata (fun msg -> msg ++ err_msg) err_msg extra_msg + extra_msg ++ err_msg | None -> print_gen ~anomaly ~extra_msg stk' e let print_gen ~anomaly (e, info) = - let extra_info = - try CList.find_map (fun f -> Some (f info)) !additional_error_info_handler - with Not_found -> None - in - let extra_msg = match extra_info with - | None -> None - | Some (loc, msg) -> msg + let extra_msg = + CList.map_filter (fun f -> f info) !additional_error_info_handler + (* Location info in the handler is ignored *) + |> List.map snd |> Pp.seq in try print_gen ~anomaly ~extra_msg !handle_stack e |