diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 15 | ||||
| -rw-r--r-- | lib/cErrors.mli | 4 | ||||
| -rw-r--r-- | lib/control.ml | 2 | ||||
| -rw-r--r-- | lib/future.ml | 2 | ||||
| -rw-r--r-- | lib/pp.ml | 6 | ||||
| -rw-r--r-- | lib/system.ml | 4 | ||||
| -rw-r--r-- | lib/util.ml | 4 | ||||
| -rw-r--r-- | lib/util.mli | 8 |
8 files changed, 16 insertions, 29 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 diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 1660a00244..f9c84b001c 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -14,7 +14,7 @@ (** {6 Error handling} *) val push : exn -> Exninfo.iexn -(** Alias for [Backtrace.add_backtrace]. *) +[@@ocaml.deprecated "please use [Exninfo.capture]"] (** {6 Generic errors.} @@ -75,5 +75,5 @@ val noncritical : exn -> bool exceptions. This method is fragile and should be considered deprecated *) val register_additional_error_info - : (Exninfo.info -> (Pp.t option Loc.located) option) + : (Exninfo.info -> Pp.t Loc.located option) -> unit diff --git a/lib/control.ml b/lib/control.ml index e67e88ee95..1898eab89e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -75,8 +75,8 @@ let windows_timeout n f x e = if not !exited then begin killed := true; raise Sys.Break end else raise e | e -> - let () = killed := true in let e = Exninfo.capture e in + let () = killed := true in Exninfo.iraise e type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } diff --git a/lib/future.ml b/lib/future.ml index ddf841b7fc..e8d232ad96 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -131,7 +131,7 @@ let rec compute ck : 'a value = let data = f () in c := Val data; `Val data with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let e = fix_exn e in match e with | (NotReady _, _) -> `Exn e @@ -201,11 +201,7 @@ let pp_with ft pp = pp_cmd s; pp_close_tag ft () [@warning "-3"] in - try pp_cmd pp - with reraise -> - let reraise = Exninfo.capture reraise in - let () = Format.pp_print_flush ft () in - Exninfo.iraise reraise + pp_cmd pp (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch diff --git a/lib/system.ml b/lib/system.ml index 2d68fd2fdf..9089eda564 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -248,9 +248,9 @@ let extern_state magic filename val_0 = marshal_out channel val_0; close_out channel with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = try_remove filename in - iraise reraise + Exninfo.iraise reraise with Sys_error s -> CErrors.user_err ~hdr:"System.extern_state" (str "System error: " ++ str s) diff --git a/lib/util.ml b/lib/util.ml index e2447b005e..ae8119ced0 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -82,10 +82,6 @@ module Set = CSet module Map = CMap -(* Stacks *) - -module Stack = CStack - (* Matrices *) let matrix_transpose mat = diff --git a/lib/util.mli b/lib/util.mli index 2f1a03a19c..be0cc11763 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -76,10 +76,6 @@ module Set : module type of CSet module Map : module type of CMap -(** {6 Stacks.} *) - -module Stack : module type of CStack - (** {6 Streams. } *) val stream_nth : int -> 'a Stream.t -> 'a @@ -119,8 +115,10 @@ val delayed_force : 'a delayed -> 'a (** {6 Enriched exceptions} *) type iexn = Exninfo.iexn +[@@ocaml.deprecated "please use [Exninfo.iexn]"] -val iraise : iexn -> 'a +val iraise : Exninfo.iexn -> 'a +[@@ocaml.deprecated "please use [Exninfo.iraise]"] (** {6 Misc. } *) |