(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
(** Additional information worn by exceptions. *)
type'a t (** Information containing a given type. *)
type info (** All information *)
type iexn = exn * info (** Information-wearing exceptions *)
val make : string -> 'a t (** Create a new piece of information. *)
val null : info (** No information *)
val add : info -> 'a t -> 'a -> info (** Add information to an exception. *)
val get : info -> 'a t -> 'a option (** Get information worn by an exception. Returns [None] if undefined. *)
val info : exn -> info (** Retrieve the information of the last exception raised. *)
type backtrace
val get_backtrace : info -> backtrace option (** [get_backtrace info] does get the backtrace associated to info *)
val backtrace_to_string : backtrace -> string (** [backtrace_to_string info] does get the backtrace associated to info *)
val record_backtrace : bool -> unit
val capture : exn -> iexn (** Add the current backtrace information and other meta-data to the given exception.
The intended use case is to re-raise an exception while preserving the meta-data: {[
try foo with | Bar -> bar | My_exn _ as exn -> let (exn, info) = Exninfo.capture err in ... let info = ... in Exninfo.iraise (exn, info)
| exn when CErrors.noncritical exn -> let iexn = Exninfo.capture err in ... Exninfo.iraise iexn
]}
where [baz] should re-raise using [iraise] below.
WARNING: any intermediate code between the [with] and the handler may modify the backtrace. Yes, that includes [when] clauses. Ideally, what you should do is something like: {[
try foo with exn when CErrors.noncritical exn -> let (err, info) = Exninfo.capture exn in match err with | exception Bar -> ... | err -> ...
]}
I admit that's a bit heavy, but there is not much to do...
*)
val iraise : iexn -> 'a (** Raise the given enriched exception. *)
val reify : unit -> info
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
