diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-16 16:57:59 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-16 17:34:57 +0200 |
| commit | 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (patch) | |
| tree | 2987141c16e3ec03afc1d3b11cb3d7b3334c6580 /stm/stm.ml | |
| parent | 26aa224293e88611dcb543e400488013bc8b30b4 (diff) | |
Undo prints only if coqtop || emacs
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e5e156a4d..449f5897e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1362,6 +1362,9 @@ let known_state ?(redefine_qed=false) ~cache id = inject_non_pstate s ), cache in + let cache_step = + if !Flags.async_proofs_cache = Some Flags.Force then `Yes + else cache_step in if Flags.async_proofs_is_master () then Pp.feedback ~state_id:id Feedback.ProcessingInMaster; State.define ~cache:cache_step ~redefine:redefine_qed step id; @@ -1470,7 +1473,8 @@ end = struct let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - if n = 1 && !Flags.coqtop_ui then VtStm (VtBack oid, false), VtNow + if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode then + VtStm (VtBack oid, false), VtNow else VtStm (VtBack oid, true), VtLater | VernacUndoTo _ | VernacRestart as e -> @@ -1684,7 +1688,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); VCS.commit id (Alias oid); - Pp.msg_notice (pr_open_cur_subgoals ()); + 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); |