diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-04 11:38:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-04 16:19:17 +0100 |
| commit | e11854569b855ae4d675e560d807ec14b8b607bf (patch) | |
| tree | b5ffa735f1c5f5ef5317fe3f70c645ab3c2c8894 /stm | |
| parent | 964024bf87a87b0e87d8891b3090083ea49b1d03 (diff) | |
Trying a new policy for when to automatically print goals (granting
the non-verbose mode which I guess one wants to obey whatever
interface is used, and restoring a policy ok for coqtop - maybe would
need a change if obeying the local verbose flag is not ok for PG or
Jedit).
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 83926adcc..94987bdb9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2322,10 +2322,10 @@ let interp verb (_,e as lexpr) = !Flags.compilation_mode = Flags.BuildVo) then let vcs = VCS.backup () in let print_goals = - (if !Flags.print_emacs then Flags.is_verbose () else !Flags.coqtop_ui) && - match clas with - | VtQuery _, _ -> false - | _ -> true in + verb && match clas with + | VtQuery _, _ -> false + | VtProofStep _, _ -> true + | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in try finish ~print_goals () with e -> let e = Errors.push e in |