diff options
| -rw-r--r-- | lib/util.ml | 2 | ||||
| -rw-r--r-- | lib/util.mli | 2 | ||||
| -rw-r--r-- | toplevel/cerrors.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
4 files changed, 7 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml index a7d2099f1..5c56fbf9b 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -22,6 +22,8 @@ let errorlabstrm l pps = raise (UserError(l,pps)) let todo s = prerr_string ("TODO: "^s^"\n") +exception Timeout + type loc = Compat.loc let dummy_loc = Compat.dummy_loc let unloc = Compat.unloc diff --git a/lib/util.mli b/lib/util.mli index 34e91215a..23fdd7670 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -32,6 +32,8 @@ val errorlabstrm : string -> std_ppcmds -> 'a val todo : string -> unit +exception Timeout + type loc = Compat.loc type 'a located = loc * 'a diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index f34621216..4250040ec 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -45,6 +45,8 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") + | Timeout -> + hov 0 (str "Timeout!") | Anomaly (s,pps) -> hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ()) | Match_failure(filename,pos1,pos2) -> diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index fad6d8e98..ee962334e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -51,7 +51,7 @@ let real_error = function | Error_in_file (_, _, e) -> e | e -> e -let timeout_handler _ = error "Timeout!" +let timeout_handler _ = raise Timeout (* 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. |