diff options
| -rw-r--r-- | lib/future.ml | 20 | ||||
| -rw-r--r-- | lib/future.mli | 3 |
2 files changed, 16 insertions, 7 deletions
diff --git a/lib/future.ml b/lib/future.ml index 02d3702d7..78a158264 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -11,21 +11,27 @@ let freeze = ref (fun () -> assert false : unit -> Dyn.t) let unfreeze = ref (fun _ -> () : Dyn.t -> unit) let set_freeze f g = freeze := f; unfreeze := g -exception NotReady of string -exception NotHere of string -let _ = Errors.register_handler (function - | NotReady name -> +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 "^ - "coqc.") - | NotHere name -> + "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 "^ - "coqc.") + "coqc.")) + +let customize_not_ready_msg f = not_ready_msg := f +let customize_not_here_msg f = not_here_msg := f + +exception NotReady of string +exception NotHere of string +let _ = Errors.register_handler (function + | NotReady name -> !not_ready_msg name + | NotHere name -> !not_here_msg name | _ -> raise Errors.Unhandled) type fix_exn = Exninfo.iexn -> Exninfo.iexn diff --git a/lib/future.mli b/lib/future.mli index 324d5f7d1..de2282ae9 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -161,3 +161,6 @@ val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds Thy are set for the outermos layer of the system, since they have to deal with the whole system state. *) val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit + +val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit +val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit |