From f7e9e6428842dd80549a0dcd20bf872c2dd7fa8c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 30 Sep 2015 22:18:56 +0200
Subject: STM: for PIDE based UIs, edit_at requires no Reach.known_state

---
 stm/stm.ml  |  3 ++-
 stm/stm.mli | 10 ++++++----
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index ed7c234c1e..d25466e089 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2342,7 +2342,8 @@ let edit_at id =
     VCS.delete_cluster_of id;
     VCS.gc ();
     VCS.print ();
-    Reach.known_state ~cache:(interactive ()) id;
+    if not !Flags.async_proofs_full then
+      Reach.known_state ~cache:(interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
   try
diff --git a/stm/stm.mli b/stm/stm.mli
index 1d926e998e..4bad7f0a6d 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -35,7 +35,9 @@ val query :
    new document tip, the document between [id] and [fo.stop] has been dropped.
    The portion between [fo.stop] and [fo.tip] has been kept.  [fo.start] is
    just to tell the gui where the editing zone starts, in case it wants to
-   graphically denote it.  All subsequent [add] happen on top of [id]. *)
+   graphically denote it.  All subsequent [add] happen on top of [id].
+   If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
+*)
 type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
 val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
 
@@ -49,11 +51,11 @@ val stop_worker : string -> unit
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
 
-(* Saves on the dist a .vio corresponding to the current status:
-   - if the worker prool is empty, all tasks are saved
+(* Saves on the disk a .vio corresponding to the current status:
+   - if the worker pool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
-     of the completed tasks is a failuere) *)
+     of the completed tasks is a failure) *)
 val snapshot_vio : DirPath.t -> string -> unit
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
-- 
cgit v1.2.3