diff options
| author | Pierre-Marie Pédrot | 2015-10-09 10:31:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-09 10:31:13 +0200 |
| commit | eb7da0d0a02a406c196214ec9d08384385541788 (patch) | |
| tree | efe031d7df32573abd7b39afa0f009a6d61f18d5 /lib/future.ml | |
| parent | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (diff) | |
| parent | 73daf37ccc7a44cd29c9b67405111756c75cb26a (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'lib/future.ml')
| -rw-r--r-- | lib/future.ml | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/lib/future.ml b/lib/future.ml index 02d3702d77..78a158264b 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 |