diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-09-28 16:50:25 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-08 09:51:13 +0200 |
| commit | 173f07a8386bf4d3d45b49d3dc01ab047b3ad4f9 (patch) | |
| tree | a079264767b207b20d5198c3f1c498fbfdd422f0 /lib/future.ml | |
| parent | 0de499ab4702708ddfae162389617869b170c7d7 (diff) | |
Future: make not-here/not-ready messages customizable
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 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 |