STM: after every command restore the expected proof mode

1 files changed, 9 insertions, 2 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 473065bed..f1ff254f0 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1896,9 +1896,16 @@ let observe id =
     iraise e
 
 let finish ?(print_goals=false) () =
-  observe (VCS.get_branch_pos (VCS.current_branch ()));
+  let head = VCS.current_branch () in
+  observe (VCS.get_branch_pos head);
   if print_goals then msg_notice (pr_open_cur_subgoals ());
-  VCS.print ()
+  VCS.print ();
+  (* Some commands may by side effect change the proof mode *)
+  match VCS.get_branch head with
+  | { VCS.kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode
+  | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
+  | _ -> ()
+
 
 let wait () =
   Slaves.wait_all_done ();