diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-04 19:22:47 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-04 19:22:47 +0000 |
| commit | 3c5b5a0871fc9af4730da06113e85bea5234ffd9 (patch) | |
| tree | b3bcae186bd1b87ee623a24d9bfa0d2a04ba44b1 /toplevel | |
| parent | 52aff80a4736ccaeb8610185959affb516a6bd9f (diff) | |
Timeout message was not always displayed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11960 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
2 files changed, 3 insertions, 1 deletions
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. |