diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-08 13:48:25 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-09 13:11:38 +0200 |
| commit | 44b3d1e0a5b51601a4b4e70e5c707dd4821e40da (patch) | |
| tree | 27d8a1e1c6a4f39cabbf78f7d33163e9956afa5f | |
| parent | 5578fb7245540a757e319a8343d1cbbff9276490 (diff) | |
Back: print subgoals as in 8.4 (Close: 3585)
| -rw-r--r-- | stm/stm.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 5c9e1cf60..da2d0fb38 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -74,6 +74,10 @@ let vernac_parse ?newtip eid s = raise e) () +let pr_open_cur_subgoals () = + try Printer.pr_open_subgoals () + with Proof_global.NoCurrentProof -> Pp.str"" + module Vcs_ = Vcs.Make(Stateid) type future_proof = Proof_global.closed_proof_output Future.computation type proof_mode = string @@ -1680,12 +1684,14 @@ 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 ()); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> prerr_endline ("undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); - Reach.known_state ~cache:(interactive ()) id; `Ok + Reach.known_state ~cache:(interactive ()) id; + Pp.msg_notice (pr_open_cur_subgoals ()); `Ok | VtStm (VtBack id, false), VtLater -> anomaly(str"classifier: VtBack + VtLater must imply part_of_script") |