diff options
| author | Enrico Tassi | 2015-09-01 12:49:52 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-09-01 12:49:52 +0200 |
| commit | ae8f843303060e1db96f72b42d744b8b200b0968 (patch) | |
| tree | d156f610fdf2b6ba89ec58266498d0c6512f3725 | |
| parent | 76d6a8cfb0448ade98e1a7abc92ff1bf5075fe8f (diff) | |
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.
| -rw-r--r-- | stm/stm.ml | 4 |
1 files 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 | _ -> () |