From 56b5573f5e5da78558e7b466e14f71a54af7b65c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 13 Mar 2014 15:59:49 +0100
Subject: STM: perspective (tell the scheduler what the user sees)

---
 toplevel/stm.ml  | 15 +++++++++++++++
 toplevel/stm.mli |  3 +++
 2 files changed, 18 insertions(+)

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.
-- 
cgit v1.2.3