STM: perspective (tell the scheduler what the user sees)

2 files changed, 18 insertions, 0 deletions

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index f6564e8921..77e8bba2d8 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -660,6 +660,8 @@ module Slaves : sig
 
   val cancel_worker : int -> unit
 
+  val set_perspective : Stateid.t list -> unit
+
 end = struct (* {{{ *)
 
 
@@ -864,6 +866,17 @@ end = struct (* {{{ *)
 
   let queue : task TQueue.t = TQueue.create ()
 
+  let set_perspective idl =
+    let open Stateid in
+    let p = List.fold_right Set.add idl Set.empty in
+    TQueue.reorder queue (fun task1 task2 ->
+      let TaskBuildProof (_, a1, b1, _, _,_,_,_) = task1 in
+      let TaskBuildProof (_, a2, b2, _, _,_,_,_) = task2 in
+      match Set.mem a1 p || Set.mem b1 p, Set.mem a2 p || Set.mem b2 p with
+      | true, true | false, false -> 0
+      | true, false -> -1
+      | false, true -> 1)
+
   let wait_all_done () =
     if not (WorkersPool.is_empty ()) then
       TQueue.wait_until_n_are_waiting_and_queue_empty
@@ -1789,6 +1802,8 @@ let add ~ontop ?(check=ignore) verb eid s =
     anomaly(str"Not yet implemented, the GUI should not try this")
   end
 
+let set_perspective id_list = Slaves.set_perspective id_list
+
 type focus = {
   start : Stateid.t;
   stop : Stateid.t;
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index cd9245895b..3414ba4f41 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -63,6 +63,9 @@ val slave_init_stdout : unit -> unit
 (* Filename *)
 val set_compilation_hints : string -> unit
 
+(* Reorders the task queue putting forward what is in the perspective *)
+val set_perspective : Stateid.t list -> unit
+
 (** read-eval-print loop compatible interface ****************************** **)
 
 (* Adds a new line to the document.  It replaces the core of Vernac.interp.