From 7fc3adcf583cea7db6a224d9a58554b19d41cd4c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 20 Feb 2015 16:01:12 +0100
Subject: Future: human readable name for delegated (Close #4065)

---
 stm/stm.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 43db6f3f6c..a4db934b25 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1270,7 +1270,7 @@ end = struct (* {{{ *)
     if TaskQueue.n_workers (Option.get !queue) = 0 then
       if !Flags.compilation_mode = Flags.BuildVio then begin
         let f,assign =
-          Future.create_delegate ~blocking:true (State.exn_on id ~valid) in
+         Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in
         let t_uuid = Future.uuid f in
         let task = ProofTask.(BuildProof {
           t_exn_info; t_start = start; t_stop = stop;
@@ -1281,7 +1281,7 @@ end = struct (* {{{ *)
       end else
         ProofTask.build_proof_here t_exn_info loc stop, cancel_switch
     else 
-      let f, t_assign = Future.create_delegate (State.exn_on id ~valid) in
+      let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
       let t_uuid = Future.uuid f in
       feedback (Feedback.InProgress 1);
       let task = ProofTask.(BuildProof {
@@ -1436,7 +1436,10 @@ end = struct (* {{{ *)
       let goals, _, _, _, _ = Proof.proof p in
       let open TacTask in
       let res = CList.map_i (fun i g ->
-        let f,assign= Future.create_delegate (State.exn_on id ~valid:safe_id) in
+        let f, assign =
+          Future.create_delegate
+            ~name:(Printf.sprintf "subgoal %d" i)
+            (State.exn_on id ~valid:safe_id) in
         let t_ast =
           { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
         let t_name = Goal.uid g in
-- 
cgit v1.2.3