diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-17 21:46:52 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-17 21:46:52 +0000 |
commit | a2f26ddde0c5ee088a4a65ab9708085c16a8ba48 (patch) | |
tree | 3e6d60a9286333416bf34151ff6d567ef5179998 /toplevel/vernac.ml | |
parent | e3c880264bf54083b962d41a4c6e1ef35ca464f2 (diff) |
An option "Set Default Timeout n."
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r-- | toplevel/vernac.ml | 65 |
1 files changed, 52 insertions, 13 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 2293707e2..e77dba790 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -51,8 +51,51 @@ let real_error = function | Error_in_file (_, _, e) -> e | e -> e +(** Timeout handling *) + +(** A global default timeout, controled by option "Set Default Timeout n". + Use "Unset Default Timeout" to deactivate it (or set it to 0). *) + +let default_timeout = ref None + +let _ = + Goptions.declare_int_option + { Goptions.optsync = true; + Goptions.optname = "the default timeout"; + Goptions.optkey = ["Default";"Timeout"]; + Goptions.optread = (fun () -> !default_timeout); + Goptions.optwrite = ((:=) default_timeout) } + +(** When interpreting a command, the current timeout is initially + the default one, but may be modified locally by a Timeout command. *) + +let current_timeout = ref None + +(** Installing and de-installing a timer. + Note: according to ocaml documentation, Unix.alarm isn't available + for native win32. *) + let timeout_handler _ = raise Timeout +let set_timeout n = + let psh = + Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + ignore (Unix.alarm n); + Some psh + +let default_set_timeout () = + match !current_timeout with + | Some n -> set_timeout n + | None -> None + +let restore_timeout = function + | None -> () + | Some psh -> + (* stop alarm *) + ignore(Unix.alarm 0); + (* restore handler *) + Sys.set_signal Sys.sigalrm psh + (* Opening and closing a channel. Open it twice when verbose: the first channel is used to read the commands, and the second one to print them. Note: we could use only one thanks to seek_in, but seeking on and on in @@ -184,25 +227,21 @@ let rec vernac_com interpfun (loc,com) = | VernacTimeout(n,v) -> if not !just_parsing then begin - let psh = - Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in - ignore (Unix.alarm n); - let stop() = - (* stop alarm *) - ignore(Unix.alarm 0); - (* restore handler *) - Sys.set_signal Sys.sigalrm psh in - try interp v; stop() - with e -> stop(); raise e + current_timeout := Some n; + interp v end | v -> if not !just_parsing then - States.with_heavy_rollback interpfun - Cerrors.process_vernac_interp_error v - + let psh = default_set_timeout () in + try + States.with_heavy_rollback interpfun + Cerrors.process_vernac_interp_error v; + restore_timeout psh + with e -> restore_timeout psh; raise e in try + current_timeout := !default_timeout; if do_beautify () then pr_new_syntax loc (Some com); interp com with e -> |