diff options
| author | Enrico Tassi | 2014-10-27 11:41:49 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-27 11:41:49 +0100 |
| commit | 9655b03d8d3f2b256b6ba71eb4b48bd767d4974b (patch) | |
| tree | 6899a28dfac21a8bce3c1171019baaf1deb6cd7f | |
| parent | b56ec63bf021a8dd95ce2eddc365115ce818a43e (diff) | |
Fixes for PG (Close 3763, 3770)
- Show does not print the goal twice
- Undo is considered as part of the document when PG mode
(bug introduced when Undo was said not to be part of the document in
coqtop mode).
| -rw-r--r-- | stm/stm.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 78f7682a39..64cf9bad72 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1513,7 +1513,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 && not !Flags.batch_mode then + if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode && + not !Flags.print_emacs then VtStm (VtBack oid, false), VtNow else VtStm (VtBack oid, true), VtLater | VernacUndoTo _ @@ -1746,8 +1747,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = prerr_endline ("undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); - Reach.known_state ~cache:(interactive ()) id; - Pp.msg_notice (pr_open_cur_subgoals ()); `Ok + Reach.known_state ~cache:(interactive ()) id; `Ok | VtStm (VtBack id, false), VtLater -> anomaly(str"classifier: VtBack + VtLater must imply part_of_script") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e04cad5c4a..90689aee6f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1686,7 +1686,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) = let vernac_show = function | ShowGoal goalref -> let info = match goalref with - | OpenSubgoals -> pr_open_subgoals () + | OpenSubgoals -> mt() (* the STM prints it *) | NthGoal n -> pr_nth_open_subgoal n | GoalId id -> pr_goal_by_id id in |