diff options
Diffstat (limited to 'lib')
51 files changed, 155 insertions, 185 deletions
diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml index 669605dec7..dc5241b89e 100644 --- a/lib/acyclicGraph.ml +++ b/lib/acyclicGraph.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli index fc648e63e9..e9f05ed74d 100644 --- a/lib/acyclicGraph.mli +++ b/lib/acyclicGraph.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 1aeca57fc1..56decb1e7d 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/aux_file.mli b/lib/aux_file.mli index b241fdc6cc..c069c417e8 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/cAst.ml b/lib/cAst.ml index b077567faf..18fa1c9b0d 100644 --- a/lib/cAst.ml +++ b/lib/cAst.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/cAst.mli b/lib/cAst.mli index 0a0b07f51b..2e07d1cd78 100644 --- a/lib/cAst.mli +++ b/lib/cAst.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index b9735d0579..d1548ab12e 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -12,7 +12,7 @@ open Pp (** Aliases *) -let push = Backtrace.add_backtrace +let push = Exninfo.capture (* Errors *) @@ -51,12 +51,10 @@ let raw_anomaly e = match e with | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." -let print_backtrace e = match Backtrace.get_backtrace e with +let print_backtrace e = match Exninfo.get_backtrace e with | None -> mt () | Some bt -> - let bt = Backtrace.repr bt in - let pr_frame f = str (Backtrace.print_frame f) in - let bt = prlist_with_sep fnl pr_frame bt in + let bt = str (Exninfo.backtrace_to_string bt) in fnl () ++ hov 0 bt let print_anomaly askreport e = @@ -68,12 +66,10 @@ let print_anomaly askreport e = let handle_stack = ref [] -exception Unhandled - let register_handler h = handle_stack := h::!handle_stack let is_handled e = - let is_handled_by h = (try let _ = h e in true with | Unhandled -> false) in + let is_handled_by h = Option.has_some (h e) in List.exists is_handled_by !handle_stack let is_anomaly = function @@ -83,37 +79,35 @@ 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 all the handlers of a list, and finally a [bottom] handler if all others have failed *) -let rec print_gen ~anomaly ~extra_msg stk (e, info) = +let rec print_gen ~anomaly ~extra_msg stk e = match stk with | [] -> print_anomaly anomaly e | h::stk' -> - try - let err_msg = h e in - Option.cata (fun msg -> msg ++ err_msg) err_msg extra_msg - with - | Unhandled -> print_gen ~anomaly ~extra_msg stk' (e,info) - | any -> print_gen ~anomaly ~extra_msg stk' (any,info) + match h e with + | Some err_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, info = match extra_info with - | None -> None, info - | Some (loc, msg) -> - let info = Option.cata (fun l -> Loc.add_loc info l) info loc in - msg, info + 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 - print_gen ~anomaly ~extra_msg !handle_stack (e,info) + try + print_gen ~anomaly ~extra_msg !handle_stack e + with exn -> + (* exception in error printer *) + str "<in exception printer>" ++ fnl () ++ print_anomaly anomaly exn (** The standard exception printer *) let iprint (e, info) = @@ -132,8 +126,8 @@ let print_no_report e = iprint_no_report (e, Exninfo.info e) let _ = register_handler begin function | UserError(s, pps) -> - where s ++ pps - | _ -> raise Unhandled + Some (where s ++ pps) + | _ -> None end (** Critical exceptions should not be caught and ignored by mistake diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 02eaf6bd0b..21d41c996d 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -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.} @@ -46,19 +46,14 @@ exception Timeout recent first) until a handle deals with it. Handles signal that they don't deal with some exception - by raising [Unhandled]. + by returning None. Raising any other exception is + forbidden and will result in an anomaly. - Handles can raise exceptions themselves, in which - case, the exception is passed to the handles which - were registered before. - - The exception that are considered anomalies should not be + Exceptions that are considered anomalies should not be handled by registered handlers. *) -exception Unhandled - -val register_handler : (exn -> Pp.t) -> unit +val register_handler : (exn -> Pp.t option) -> unit (** The standard exception printer *) val print : exn -> Pp.t @@ -80,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/cProfile.ml b/lib/cProfile.ml index 34656ef4d5..a4f2da7080 100644 --- a/lib/cProfile.ml +++ b/lib/cProfile.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/cProfile.mli b/lib/cProfile.mli index 50dd6bec34..9ff384af96 100644 --- a/lib/cProfile.mli +++ b/lib/cProfile.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 0f2c083042..cc1fa647f9 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index 1938cab4d7..ded1f9be3b 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/control.ml b/lib/control.ml index 7d54838df8..bb42b5727e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -38,7 +38,7 @@ let unix_timeout n f x e = restore_timeout (); res with e -> - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in restore_timeout (); Exninfo.iraise e @@ -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 e = Exninfo.capture e in let () = killed := true in - let e = Backtrace.add_backtrace e in Exninfo.iraise e type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } @@ -102,7 +102,7 @@ let protect_sigalrm f x = | true, Sys.Signal_handle f -> f Sys.sigalrm; res | _, _ -> res with e -> - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in Sys.set_signal Sys.sigalrm old_handler; Exninfo.iraise e with Invalid_argument _ -> (* This happens on Windows, as handling SIGALRM does not seem supported *) diff --git a/lib/control.mli b/lib/control.mli index 18a84e698f..25135934bc 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index 4c670f6abe..86e74d1a56 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index bd8952b8fc..7ca7b8d6c4 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/dAst.ml b/lib/dAst.ml index a9a92b3ed7..70c6cc7977 100644 --- a/lib/dAst.ml +++ b/lib/dAst.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/dAst.mli b/lib/dAst.mli index 599ad0219b..4315db9f84 100644 --- a/lib/dAst.mli +++ b/lib/dAst.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/envars.ml b/lib/envars.ml index 67759d0a3e..c9c97eaa97 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/envars.mli b/lib/envars.mli index 9f65ef8557..13aae47329 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/explore.ml b/lib/explore.ml index 42d48fbc1b..b3ffef6ac2 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/explore.mli b/lib/explore.mli index 6dc2e358d2..2db6cd0dd6 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/feedback.ml b/lib/feedback.ml index 8ba6489dc5..0dff28a1e5 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/feedback.mli b/lib/feedback.mli index 5375d97d57..e4d6b229d1 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/flags.ml b/lib/flags.ml index 1fe52c3b95..1d9d6d49bc 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -19,7 +19,7 @@ let with_modified_ref ?(restore=true) r nf f x = if restore || pre == !r then r := old_ref; res with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in r := old_ref; Exninfo.iraise reraise @@ -37,7 +37,7 @@ let with_options ol f x = let r = f x in let () = List.iter2 (:=) ol vl in r with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise diff --git a/lib/flags.mli b/lib/flags.mli index 0e438e2358..30d1b5b2bd 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/future.ml b/lib/future.ml index d3ea538549..661637fcd1 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -12,13 +12,13 @@ let not_ready_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ - "asynchronous script processing and don't pass \"-quick\" to "^ + "asynchronous script processing and don't pass \"-vio\" to "^ "coqc.")) let not_here_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not available "^ "in this process. If you really need this, pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ - "asynchronous script processing and don't pass \"-quick\" to "^ + "asynchronous script processing and don't pass \"-vio\" to "^ "coqc.")) let customize_not_ready_msg f = not_ready_msg := f @@ -28,9 +28,9 @@ exception NotReady of string exception NotHere of string let _ = CErrors.register_handler (function - | NotReady name -> !not_ready_msg name - | NotHere name -> !not_here_msg name - | _ -> raise CErrors.Unhandled) + | NotReady name -> Some (!not_ready_msg name) + | NotHere name -> Some (!not_here_msg name) + | _ -> None) type fix_exn = Exninfo.iexn -> Exninfo.iexn let id x = x @@ -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 diff --git a/lib/future.mli b/lib/future.mli index c0fc91bcc3..7a85c37970 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/genarg.ml b/lib/genarg.ml index 152d00bf7c..25c37977dc 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/genarg.mli b/lib/genarg.mli index 3e681ad2b9..88e9ff13e8 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/hook.ml b/lib/hook.ml index 76da1071b8..8782d3a2c8 100644 --- a/lib/hook.ml +++ b/lib/hook.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/hook.mli b/lib/hook.mli index e3eb370ecb..5b92c62954 100644 --- a/lib/hook.mli +++ b/lib/hook.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/loc.ml b/lib/loc.ml index 13a7fdea3e..09fa45a884 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/loc.mli b/lib/loc.mli index 6a86005c7b..c54a837bb4 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -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 = Backtrace.add_backtrace 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/pp.mli b/lib/pp.mli index 7bb66b0135..b265537728 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml index 8a7934d552..988e8e4303 100644 --- a/lib/pp_diff.ml +++ b/lib/pp_diff.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli index 24f2eace93..42db6aee43 100644 --- a/lib/pp_diff.mli +++ b/lib/pp_diff.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index d7c08957b9..5e1150146e 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli index ef6f34c525..42d1f8a8d1 100644 --- a/lib/remoteCounter.mli +++ b/lib/remoteCounter.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/rtree.ml b/lib/rtree.ml index 9709540059..9c7c85e72e 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/rtree.mli b/lib/rtree.mli index 9887580e7a..3dae89e7f8 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/spawn.ml b/lib/spawn.ml index 046829802b..2fe7b31d04 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/spawn.mli b/lib/spawn.mli index 03613fc4ec..34a2cee31b 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/stateid.ml b/lib/stateid.ml index 023d782325..a1328f156c 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/stateid.mli b/lib/stateid.mli index f73a210249..9b2de9c894 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/system.ml b/lib/system.ml index 2d68fd2fdf..d7f5fa26ab 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -11,7 +11,6 @@ (* $Id$ *) open Pp -open Util include Minisys @@ -42,15 +41,7 @@ let all_subdirs ~unix_path:root = (* Caching directory contents for efficient syntactic equality of file names even on case-preserving but case-insensitive file systems *) -module StrMod = struct - type t = string - let compare = compare -end - -module StrMap = Map.Make(StrMod) -module StrSet = Set.Make(StrMod) - -let dirmap = ref StrMap.empty +let dirmap = ref CString.Map.empty let make_dir_table dir = let entries = @@ -59,8 +50,8 @@ let make_dir_table dir = with Sys_error _ -> warn_cannot_open_dir dir; [||] in - let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in - Array.fold_left filter_dotfiles StrSet.empty entries + let filter_dotfiles s f = if f.[0] = '.' then s else CString.Set.add f s in + Array.fold_left filter_dotfiles CString.Set.empty entries (** Don't trust in interactive mode (the default) *) let trust_file_cache = ref false @@ -68,20 +59,20 @@ let trust_file_cache = ref false let exists_in_dir_respecting_case dir bf = let cache_dir dir = let contents = make_dir_table dir in - dirmap := StrMap.add dir contents !dirmap; + dirmap := CString.Map.add dir contents !dirmap; contents in let contents, fresh = try (* in batch mode, assume the directory content is still fresh *) - StrMap.find dir !dirmap, !trust_file_cache + CString.Map.find dir !dirmap, !trust_file_cache with Not_found -> (* in batch mode, we are not yet sure the directory exists *) - if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true + if !trust_file_cache && not (exists_dir dir) then CString.Set.empty, true else cache_dir dir, true in - StrSet.mem bf contents || + CString.Set.mem bf contents || not fresh && (* rescan, there is a new file we don't know about *) - StrSet.mem bf (cache_dir dir) + CString.Set.mem bf (cache_dir dir) let file_exists_respecting_case path f = (* This function ensures that a file with expected lowercase/uppercase @@ -248,9 +239,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/system.mli b/lib/system.mli index a56479e3b4..00701379bd 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) diff --git a/lib/util.ml b/lib/util.ml index e2447b005e..87cc30e557 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -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..fe34525671 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -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. } *) diff --git a/lib/xml_datatype.mli b/lib/xml_datatype.mli index 8f14100d6b..43ebff1ce9 100644 --- a/lib/xml_datatype.mli +++ b/lib/xml_datatype.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) |