From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 19 Apr 2011 16:44:20 +0200
Subject: Imported Upstream version 8.3.pl2

---
 toplevel/search.ml        |  5 ++--
 toplevel/vernac.ml        | 67 +++++++++++++++++++++++++++++++++++++----------
 toplevel/vernacentries.ml |  6 ++---
 3 files changed, 58 insertions(+), 20 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/search.ml b/toplevel/search.ml
index 0bd552af..574983cd 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: search.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: search.ml 13853 2011-02-24 07:57:31Z glondu $ *)
 
 open Pp
 open Util
@@ -197,7 +197,8 @@ let filter_by_module_from_list = function
   | l, outside -> filter_by_module l (not outside)
 
 let filter_subproof gr _ _ =
-  not (string_string_contains (name_of_reference gr) "_subproof")
+  not (string_string_contains (name_of_reference gr) "_subproof") &&
+  not (string_string_contains (name_of_reference gr) "_admitted")
 
 let (&&&&&) f g x y z = f x y z && g x y z
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9464d763..afc5057e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 13668 2010-12-02 17:43:59Z herbelin $ *)
+(* $Id: vernac.ml 13923 2011-03-21 16:25:20Z letouzey $ *)
 
 (* Parsing of vernacular. *)
 
@@ -52,8 +52,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
@@ -185,25 +228,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 ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d74711c2..7710cb95 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 13492 2010-10-04 21:20:01Z herbelin $ i*)
+(*i $Id: vernacentries.ml 13922 2011-03-21 16:25:18Z letouzey $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -1013,9 +1013,7 @@ let vernac_set_option locality key = function
   | BoolValue b -> set_bool_option_value_gen locality key b
 
 let vernac_unset_option locality key =
-  try set_bool_option_value_gen locality key false
-  with _ ->
-  set_int_option_value_gen locality key None
+  unset_option_value_gen locality key
 
 let vernac_add_option key lv =
   let f = function
-- 
cgit v1.2.3