From b2007e86b4a28570eee52439ad8b9fee603443b8 Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 13:50:59 +0200
Subject: STM: Pass exception information to unreachable_state_hook functions

This lets hooks treat different exceptions in different ways; in
particular, user interrupts can now be safely ignored
---
 stm/stm.ml  | 4 ++--
 stm/stm.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index acbb5f646d..e96c396bae 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
 
@@ -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))
diff --git a/stm/stm.mli b/stm/stm.mli
index 4bad7f0a6d..2453f258c5 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -100,7 +100,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
 
-- 
cgit v1.2.3


From ce0c536b4430711db1e30cd7ac35ae8d71d34e64 Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 13:58:50 +0200
Subject: STM: Added functions for saving and restoring the internal state

PIDEtop needs these to implement its new transaction mechanism
---
 stm/stm.ml  | 3 +++
 stm/stm.mli | 4 ++++
 2 files changed, 7 insertions(+)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index e96c396bae..c0d71dc933 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -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 2453f258c5..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
-- 
cgit v1.2.3


From 56ca108e63191e90c3d4169c37a4c97017e3c6ae Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 14:19:34 +0200
Subject: TQueue: Expose the length of TQueues

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

(limited to 'stm')

diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 6fef895ae8..2a43cd7d13 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,6 +94,12 @@ 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;
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 7458de510f..f54af4df47 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -28,3 +28,5 @@ 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
-- 
cgit v1.2.3


From f6b3704391de97ee544da9ae7316685cd2d9fae3 Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 14:20:22 +0200
Subject: TQueue: Allow some tasks to be saved when clearing a TQueue

---
 stm/tQueue.ml  | 12 ++++++++++++
 stm/tQueue.mli |  1 +
 2 files changed, 13 insertions(+)

(limited to 'stm')

diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 2a43cd7d13..2dad962bec 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -105,6 +105,18 @@ let clear { queue = q; lock = m; cond = c } =
   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 f54af4df47..1df52d2523 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -22,6 +22,7 @@ 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
-- 
cgit v1.2.3


From 41ac12062858d3b8b82b0ed736b3800d052f34b8 Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 15:23:02 +0200
Subject: STM: Work around an occasional crash in dot (debug output)

The splines=ortho option seems to make dot crash sometimes, so this commit
removes it from the STM debugging output
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index c0d71dc933..5bb46fd368 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -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) ->
-- 
cgit v1.2.3