An option "Set Default Timeout n."

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 68 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index 6cac125b19..c7d3fb2915 100644
--- a/CHANGES
+++ b/CHANGES
@@ -26,6 +26,7 @@ Vernacular commands
 - New command "Print Sorted Universes".
 - The undocumented and obsolete option "Set/Unset Boxed Definitions" has
   been removed, as well as syntaxes like "Boxed Fixpoint foo".
+- A new option "Set Default Timeout n / Unset Default Timeout".
 
 Module System
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index ab8e1531f8..5a564b6765 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -933,6 +933,21 @@ the command has not terminated after the time specified by the integer
 (time expressed in seconds), then it is interrupted and an error message
 is displayed.
 
+\subsection[\tt Set Default Timeout \textrm{\textsl{int}}.]{\tt Set
+  Default Timeout \textrm{\textsl{int}}.\comindex{Set Default Timeout}}
+
+After using this command, all subsequent commands behave as if they
+were passed to a {\tt Timeout} command. Commands already starting by
+a {\tt Timeout} are unaffected.
+
+\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}}
+
+This command turns off the use of a defaut timeout.
+
+\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}}
+
+This command displays whether some default timeout has be set or not.
+
 \section{Controlling display}
 
 \subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent}
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 2293707e2d..e77dba7904 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 ->