diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-15 04:15:55 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-23 19:30:17 +0100 |
| commit | ed09ae7a473a99c914f2af64d3387d9190e85849 (patch) | |
| tree | e5b51993dc0602eb1fa985d293d82c03d286ec86 /toplevel/coqloop.ml | |
| parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) | |
[flags] Move global time flag into an attribute.
One less global flag.
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 910c81381..5c1b27c33 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 |