From deadfb32365e903378515b1004e5109d47720411 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 22 Mar 2015 12:07:45 +0100
Subject: STM: after every command restore the expected proof mode

---
 stm/stm.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 473065bedc..f1ff254f04 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 ();
-- 
cgit v1.2.3