diff options
| author | Enrico Tassi | 2014-11-03 10:26:27 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-11-03 10:26:31 +0100 |
| commit | 7d01d46ce0f9267446b474755762db1ccca5fd78 (patch) | |
| tree | b10cea070902b40e282d1e4f6acfafa742ebe70d | |
| parent | 6243a0b9c16562a90e0e14f60047e9b0f2a0f2e8 (diff) | |
STM: fix printing of goals when on a tty interface
| -rw-r--r-- | stm/stm.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index c9bda157f6..bb48a4f001 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1675,11 +1675,9 @@ let observe id = VCS.restore vcs; raise e -let finish () = +let finish ?(print_goals=false) () = 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 ()); + if print_goals then Pp.msg_notice (pr_open_cur_subgoals ()); VCS.print () let wait () = @@ -2131,11 +2129,18 @@ let interp verb (_,e as lexpr) = (!Flags.async_proofs_mode = Flags.APoff && !Flags.compilation_mode = Flags.BuildVo) then let vcs = VCS.backup () in - try finish () + let print_goals = + (if !Flags.print_emacs then Flags.is_verbose () else !Flags.coqtop_ui) && + match clas with + | VtQuery _, _ -> false + | _ -> true in + try finish ~print_goals () with e -> let e = Errors.push e in handle_failure e vcs true +let finish () = finish () + let get_current_state () = VCS.cur_tip () let current_proof_depth () = |