Merge branch 'v8.5'

4 files changed, 34 insertions, 4 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index c7836d118b..ea31e0410f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -51,7 +51,7 @@ let execution_error, execution_error_hook = Hook.make
     feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
- ~default:(fun _ -> ()) ()
+ ~default:(fun _ _ -> ()) ()
 
 include Hook
 
@@ -372,7 +372,7 @@ end = struct (* {{{ *)
          (try let n = Hashtbl.find clus c in from::n
          with Not_found -> [from]); true in
     let oc = open_out fname_dot in
-    output_string oc "digraph states {\nsplines=ortho\n";
+    output_string oc "digraph states {\n";
     Dag.iter graph (fun from cf _ l ->
       let c1 = add_to_clus_or_ids from cf in
       List.iter (fun (dest, trans) ->
@@ -736,7 +736,7 @@ end = struct (* {{{ *)
       let good_id = !cur_id in
       cur_id := Stateid.dummy;
       VCS.reached id false;
-      Hooks.(call unreachable_state id);
+      Hooks.(call unreachable_state id (e, info));
       match Stateid.get info, safe_id with
       | None, None -> iraise (exn_on id ~valid:good_id (e, info))
       | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info))
@@ -2405,6 +2405,9 @@ let edit_at id =
         VCS.print ();
         iraise (e, info)
 
+let backup () = VCS.backup ()
+let restore d = VCS.restore d
+
 (*********************** TTY API (PG, coqtop, coqc) ***************************)
 (******************************************************************************)
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 4bad7f0a6d..18ed6fc2e8 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -83,6 +83,10 @@ val set_compilation_hints : string -> unit
 (* Reorders the task queue putting forward what is in the perspective *)
 val set_perspective : Stateid.t list -> unit
 
+type document
+val backup : unit -> document
+val restore : document -> unit
+
 (** workers **************************************************************** **)
 
 module ProofTask : AsyncTaskQueue.Task
@@ -100,7 +104,7 @@ val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
 val parse_error_hook :
   (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
-val unreachable_state_hook : (Stateid.t -> unit) Hook.t
+val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t
 
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 6fef895ae8..2dad962bec 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -15,6 +15,7 @@ module PriorityQueue : sig
   val pop : ?picky:('a -> bool) -> 'a t -> 'a
   val push : 'a t -> 'a -> unit
   val clear : 'a t -> unit
+  val length : 'a t -> int
 end = struct
   type 'a item = int * 'a
   type 'a rel = 'a item -> 'a item -> int
@@ -38,6 +39,7 @@ end = struct
   let set_rel rel ({ contents = (xs, _) } as t) =
     let rel (_,x) (_,y) = rel x y in
     t := (List.sort rel xs, rel)
+  let length ({ contents = (l, _) }) = List.length l
 end
 
 type 'a t = {
@@ -92,11 +94,29 @@ let push { queue = q; lock = m; cond = c; release } x =
   Condition.broadcast c;
   Mutex.unlock m
 
+let length { queue = q; lock = m } =
+  Mutex.lock m;
+  let n = PriorityQueue.length q in
+  Mutex.unlock m;
+  n
+
 let clear { queue = q; lock = m; cond = c } =
   Mutex.lock m;
   PriorityQueue.clear q;
   Mutex.unlock m
 
+let clear_saving { queue = q; lock = m; cond = c } f =
+  Mutex.lock m;
+  let saved = ref [] in
+  while not (PriorityQueue.is_empty q) do
+    let elem = PriorityQueue.pop q in
+    match f elem with
+    | Some x -> saved := x :: !saved
+    | None -> ()
+  done;
+  Mutex.unlock m;
+  List.rev !saved
+
 let is_empty { queue = q } = PriorityQueue.is_empty q
 
 let destroy tq =
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 7458de510f..1df52d2523 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -22,9 +22,12 @@ val broadcast : 'a t -> unit
 val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list
 
 val clear : 'a t -> unit
+val clear_saving : 'a t -> ('a -> 'b option) -> 'b list
 val is_empty : 'a t -> bool
 
 exception BeingDestroyed
 (* Threads blocked in pop can get this exception if the queue is being
  * destroyed *)
 val destroy : 'a t -> unit
+
+val length : 'a t -> int