From ae8f843303060e1db96f72b42d744b8b200b0968 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 1 Sep 2015 12:49:52 +0200
Subject: STM: save a full state for queries.

In PIDE based UIs queries can be delegated too, hence to speed up
things I was saving a shallow state.  Unfortunately a shallow state
breaks section/modules commands, and a query can be the last entry
of a section/module.  (A shallow state does essentially drop the libstack).

The easy solution is to save a complete state.
A better one would be to refine the static analysis of the document and
decide which kind of saved state one needs.
---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index bf91c3aa4f..e6271f6089 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1773,7 +1773,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel }
         when Flags.async_proofs_is_master () -> (fun () ->
-            reach ~cache:`Shallow view.next;
+            reach view.next;
             Query.vernac_interp cancel view.next id x
           ), cache, false
       | `Cmd { cast = x } -> (fun () ->
@@ -1935,7 +1935,7 @@ let finish ?(print_goals=false) () =
   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 = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
   | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
   | _ -> ()
 
-- 
cgit v1.2.3