diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-13 03:59:13 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-13 17:57:35 +0200 |
| commit | 041cb0de6204989000352311e01847ce5a908a14 (patch) | |
| tree | 69d6810aec20e11eb90423fb6cb79490f495a398 /toplevel | |
| parent | a5c150a6a7fa980c5850aa247e62d02e29773235 (diff) | |
[toplevel] Don't print goals if there is no pending proof.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 98458a57a..18f93197c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -126,11 +126,12 @@ let rec interp_vernac sid po (loc,com) = (* Stm.observe nsid; *) Stm.finish (); - (* We could use a more refined criteria depending on the + (* We could use a more refined criteria that depends on the vernac. For now we imitate the old approach. *) - let print_goals = not (!Flags.batch_mode || is_query v) in + let hide_goals = !Flags.batch_mode || is_query v || + not (Proof_global.there_are_pending_proofs ()) in - if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); + if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); nsid with exn when CErrors.noncritical exn -> |