diff options
| author | Maxime Dénès | 2017-12-29 13:41:29 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-29 13:41:29 +0100 |
| commit | c0e5746e6b273eb4592d24867da55dde40b656c9 (patch) | |
| tree | f19c8de545f461a7cf8abfbbd7747e8020a9b8a0 /toplevel/coqloop.ml | |
| parent | 7e319ad03aba413f3165b848eaf821b364f9291b (diff) | |
| parent | ed09ae7a473a99c914f2af64d3387d9190e85849 (diff) | |
Merge PR #6433: [flags] Move global time flag into an attribute.
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 910c81381b..5c1b27c333 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -300,13 +300,13 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in is caught and handled (i.e. not re-raised). *) -let do_vernac doc sid = +let do_vernac ~time doc sid = top_stderr (fnl()); if !print_emacs then top_stderr (str (top_buffer.prompt doc)); resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.process_expr doc sid (read_sentence ~doc sid (fst input)) + Vernac.process_expr ~time doc sid (read_sentence ~doc sid (fst input)) with | Stm.End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit @@ -337,13 +337,13 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () -let rec loop doc = +let rec loop ~time doc = Sys.catch_break true; try reset_input_buffer doc stdin top_buffer; (* Be careful to keep this loop tail-recursive *) let rec vernac_loop doc sid = - let ndoc, nsid = do_vernac doc sid in + let ndoc, nsid = do_vernac ~time doc sid in loop_flush_all (); vernac_loop ndoc nsid (* We recover the current stateid, threading from the caller is @@ -358,4 +358,4 @@ let rec loop doc = fnl() ++ str"Please report" ++ strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); - loop doc + loop ~time doc |