diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-22 15:12:51 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-22 16:00:01 +0200 |
| commit | ad28bacca8cf9f779db099f7c42938b96ae31f42 (patch) | |
| tree | f0cceec16fc36bfa586bad7b0a0536215527ce5d /stm/stm.ml | |
| parent | 356597ffc42b9298e27e0af2cfd05fe73f6d1383 (diff) | |
Goal printing made uniform: always done in STM (close 3585)
Goal printing was partially broken. Some commands in vernacentries
were printing, but not all of them. Moreover an unlucky combination
of `Flags.verbosely (fun () -> interp "Set Silent")` was making the
silent flag not settable anymore.
Now STM always print the open goals after a command when run in interactive
mode via coqtop or emacs. More modern GUI do ask for the goals.
Diffstat (limited to 'stm/stm.ml')
| -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 74a998a74..78f7682a3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1589,6 +1589,9 @@ let observe id = let finish () = observe (VCS.get_branch_pos (VCS.current_branch ())); + if (not !Flags.print_emacs && !Flags.coqtop_ui && not !Flags.batch_mode) || + (!Flags.print_emacs && Flags.is_verbose ()) then + Pp.msg_notice (pr_open_cur_subgoals ()); VCS.print () let wait () = @@ -1697,7 +1700,7 @@ let reset_task_queue = Slaves.reset_task_queue let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let warn_if_pos a b = if b then msg_warning(pr_ast a ++ str" should not be part of a script") in - let v, x = expr, { verbose = verbose && Flags.is_verbose(); loc; expr } in + let v, x = expr, { verbose = verbose; loc; expr } in prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x)); let vcs = VCS.backup () in try @@ -1738,9 +1741,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); VCS.commit id (Alias oid); - if (!Flags.coqtop_ui && not !Flags.batch_mode) || - !Flags.print_emacs then - Pp.msg_notice (pr_open_cur_subgoals ()); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> prerr_endline ("undo to state " ^ Stateid.to_string id); |