From a5a333ddbf5c27320e767ca0611caf8a821449aa Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 27 Mar 2015 12:02:30 +0100
Subject: STM: refine the notion of "simply a tactic"

When a worker sends back a system state to master, it tries to
just send a delta.  If the command is a simple tactic, then only
the proof state changes.

Now, what is a simple tactic?
1. a tactic
2. that does not change the environment

Check 1. was surely incomplete.  Now it is:
  VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _
Is it complete?
---
 stm/stm.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 9e30cbbcd9..477ca1f0dc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1093,6 +1093,9 @@ end = struct (* {{{ *)
   
   let perform_states query =
     if query = [] then [] else
+    let is_tac = function
+      | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true
+      | _ -> false in
     let initial = 
       let rec aux id =
         try match VCS.visit id with { next } -> aux next
@@ -1110,8 +1113,8 @@ end = struct (* {{{ *)
         if State.is_cached id then Some (State.get_cached id) else None in
       match prev, this with
       | _, None -> None
-      | Some (prev, o, `Cmd { cast = { expr = VernacSolve _ }}), Some n
-        when State.same_env o n -> (* A pure tactic *)
+      | Some (prev, o, `Cmd { cast = { expr }}), Some n
+        when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `Proof (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
           msg_warning (str "Sending back a fat state");
-- 
cgit v1.2.3