diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 15 | ||||
| -rw-r--r-- | lib/cErrors.mli | 13 | ||||
| -rw-r--r-- | lib/future.ml | 2 | ||||
| -rw-r--r-- | lib/pp.ml | 4 | ||||
| -rw-r--r-- | lib/util.ml | 7 | ||||
| -rw-r--r-- | lib/util.mli | 7 |
6 files changed, 22 insertions, 26 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 3e1ba9107c..b9735d0579 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -25,20 +25,13 @@ let _ = in Printexc.register_printer pr -let make_anomaly ?label pp = - Anomaly (label, pp) - let anomaly ?loc ?label pp = Loc.raise ?loc (Anomaly (label, pp)) exception UserError of string option * Pp.t (* User errors *) -let todo s = prerr_string ("TODO: "^s^"\n") - let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) -let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) - exception Timeout (** Only anomalies should reach the bottom of the handler stack. @@ -123,17 +116,17 @@ let print_gen ~anomaly (e, info) = print_gen ~anomaly ~extra_msg !handle_stack (e,info) (** The standard exception printer *) -let print ?info e = - let info = Option.default Exninfo.(info e) info in +let iprint (e, info) = print_gen ~anomaly:true (e,info) ++ print_backtrace info -let iprint (e, info) = print ~info e +let print e = + iprint (e, Exninfo.info e) (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) -let print_no_report e = print_gen ~anomaly:false (e, Exninfo.info e) let iprint_no_report (e, info) = print_gen ~anomaly:false (e,info) ++ print_backtrace info +let print_no_report e = iprint_no_report (e, Exninfo.info e) (** Predefined handlers **) diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 100dcd0b22..02eaf6bd0b 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -21,9 +21,6 @@ val push : exn -> Exninfo.iexn [Anomaly] is used for system errors and [UserError] for the user's ones. *) -val make_anomaly : ?label:string -> Pp.t -> exn -(** Create an anomaly. *) - val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a (** Raise an anomaly, with an optional location and an optional label identifying the anomaly. *) @@ -41,14 +38,6 @@ val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a (** Main error raising primitive. [user_err ?loc ?hdr pp] signals an error [pp] with optional header and location [hdr] [loc] *) -val invalid_arg : ?loc:Loc.t -> string -> 'a - -(** [todo] is for running of an incomplete code its implementation is - "do nothing" (or print a message), but this function should not be - used in a released code *) - -val todo : string -> unit - exception Timeout (** [register_handler h] registers [h] as a handler. @@ -72,7 +61,7 @@ exception Unhandled val register_handler : (exn -> Pp.t) -> unit (** The standard exception printer *) -val print : ?info:Exninfo.info -> exn -> Pp.t +val print : exn -> Pp.t val iprint : Exninfo.iexn -> Pp.t (** Same as [print], except that the "Please report" part of an anomaly diff --git a/lib/future.ml b/lib/future.ml index f6e9cee140..01fb7d0297 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -68,7 +68,7 @@ and 'a computation = 'a comput ref let unnamed = "unnamed" let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = - ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x))) + ref (Ongoing (name, CEphemeron.create (uuid, f, ref x))) let get x = match !x with | Finished v -> unnamed, UUID.invalid, id, ref (Val v) @@ -197,9 +197,9 @@ let pp_with ft pp = | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms - | Ppcmd_tag(tag, s) -> pp_open_tag ft tag; + | Ppcmd_tag(tag, s) -> pp_open_tag ft tag [@warning "-3"]; pp_cmd s; - pp_close_tag ft () + pp_close_tag ft () [@warning "-3"] in try pp_cmd pp with reraise -> diff --git a/lib/util.ml b/lib/util.ml index bac06b5701..61678f7669 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -8,6 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +type 'a pervasives_ref = 'a ref +let pervasives_ref = ref +let pervasives_compare = compare +let (!) = (!) +let (+) = (+) +let (-) = (-) + (* Mapping under pairs *) let on_fst f (a,b) = (f a,b) diff --git a/lib/util.mli b/lib/util.mli index 8ccb4b3f08..b6347126e0 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -8,6 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +type 'a pervasives_ref = 'a ref +val pervasives_ref : 'a -> 'a ref +val pervasives_compare : 'a -> 'a -> int +val (!) : 'a ref -> 'a +val (+) : int -> int -> int +val (-) : int -> int -> int + (** This module contains numerous utility functions on strings, lists, arrays, etc. *) |