diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index 5cbe1c1f..e8326f53 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -63,7 +63,10 @@ let inject_em_events events = List.map inject_em_event events
 type events = event Sel.Event.t list
 
 let print_exec_overview st =
-  let {processing; processed} = st.overview in
+  let {processing; processed; prepared} = st.overview in
+  log @@ "--------- Prepared ranges ---------";
+  List.iter (fun r -> log @@ Range.to_string r) prepared;
+  log @@ "-------------------------------------";
   log @@ "--------- Processing ranges ---------";
   List.iter (fun r -> log @@ Range.to_string r) processing;
   log @@ "-------------------------------------";
@@ -362,7 +365,17 @@ let handle_event ev st =
     let overview = ExecutionManager.update_overview task todo execution_state st.document st.overview in
     (Some {st with execution_state; overview}, inject_em_events events @ [event])
   | ExecutionManagerEvent ev ->
-    let execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in
+    let id, execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in
+    let st = 
+      match (id, execution_state_update) with
+      | Some id, Some exec_st ->
+        let overview = ExecutionManager.update_processed id exec_st st.document st.overview in
+        {st with overview}
+      | Some id, None ->
+        let overview = ExecutionManager.update_processed id st.execution_state st.document st.overview in
+        {st with overview}
+      | _, _ -> st
+    in
     (Option.map (fun execution_state -> {st with execution_state}) execution_state_update, inject_em_events events)
 
 let get_proof st diff_mode pos =
diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 8f547b19..ef0d8490 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -240,7 +240,7 @@ let rec insert_or_merge_range r = function
 
 let rec remove_or_truncate_range r = function
 | [] -> []
-| r1 :: l ->
+| r1 :: l -> log @@ "RANGES"; log @@ "R1: " ^ Range.to_string r1; log @@ "R: " ^ Range.to_string r;
   if Position.compare r1.Range.start r.Range.start == 0 && 
     Position.compare r1.Range.end_ r.Range.end_ == 0
   then
@@ -251,60 +251,72 @@ let rec remove_or_truncate_range r = function
   else
     r1 :: (remove_or_truncate_range r l)
 
-let update_processed task state processing processed prepared document =
-  match task with
-  | PDelegate {opener_id; terminator_id; } ->
-    let opener_range = Document.range_of_id_with_blank_space document opener_id in
-    let terminator_range = Document.range_of_id_with_blank_space document terminator_id in
-    let range = Range.create ~end_:terminator_range.end_ ~start:opener_range.start in
-    begin match SM.find terminator_id state.of_sentence with
-    | (s, _) ->
-      begin match s with
-      | Done s ->
-        begin match s with
-        | Success _ ->
-          insert_or_merge_range range processed, remove_or_truncate_range range processing, remove_or_truncate_range range prepared
-        | Error _ ->
-          processed, remove_or_truncate_range range processing, remove_or_truncate_range range prepared
-        end
-      | _ -> processed, processing, prepared
-      end
-    | exception Not_found ->
-      log @@ "Trying to get overview with non-existing state id " ^ Stateid.to_string terminator_id;
-      processed, processing, prepared
+let update_processed_as_Done s range overview =
+  let {prepared; processing; processed} = overview in
+  match s with
+  | Success _ ->
+    log @@ "INSERTING TO PROCESSED";
+    let processed = insert_or_merge_range range processed in
+    log @@ "TRUNCATING FROM PROCESSING";
+    let processing = remove_or_truncate_range range processing in
+    log @@ "TRUNCATING FROM PREPARED";
+    let prepared = remove_or_truncate_range range prepared in
+    {prepared; processing; processed}
+  | Error _ ->
+    log @@ "TRUNCATING FROM PROCESSING";
+    let processing = remove_or_truncate_range range processing in
+    log @@ "TRUNCATING FROM PREPARED";
+    let prepared = remove_or_truncate_range range prepared in
+    {prepared; processing; processed}
+
+let update_processed id state document overview =
+  log @@ "UPDATING PROCESSED";
+  let range = Document.range_of_id_with_blank_space document id in
+  match SM.find id state.of_sentence with
+  | (s, _) ->
+    begin match s with
+    | Done s -> update_processed_as_Done s range overview
+    | _ -> assert false (* delegated sentences born as such, cannot become it later *)
     end
-  | PSkip { id } | PExec { id } | PQuery { id } ->
-    let range = Document.range_of_id_with_blank_space document id in
-    match SM.find id state.of_sentence with
-    | (s, _) ->
-      begin match s with
-      | Done s ->
-        begin match s with
-        | Success _ ->
-          insert_or_merge_range range processed, remove_or_truncate_range range processing, remove_or_truncate_range range prepared
-        | Error _ ->
-          processed, remove_or_truncate_range range processing, remove_or_truncate_range range prepared
-        end
-      | _ -> processed, processing, prepared
-      end
-    | exception Not_found ->
-      log @@ "Trying to get overview with non-existing state id " ^ Stateid.to_string id;
-      processed, processing, prepared
+  | exception Not_found ->
+    log @@ "Trying to get overview with non-existing state id " ^ Stateid.to_string id;
+    overview
 
 let update_processing task processing prepared document =
+  log @@ "UPDATING PROCESSING";
   match task with
-  | PDelegate { opener_id; terminator_id; } ->
-    let opener_range = Document.range_of_id_with_blank_space document opener_id in
-    let terminator_range = Document.range_of_id_with_blank_space document terminator_id in
-    let range = Range.create ~end_:terminator_range.end_ ~start:opener_range.start in
-    insert_or_merge_range range processing, remove_or_truncate_range range prepared
+  | PDelegate { opener_id; terminator_id; tasks } ->
+    let proof_opener_id = match tasks with
+      | [] -> opener_id
+      | (PSkip { id } | PExec { id } | PQuery { id }) :: _ -> id
+      | PDelegate _ :: _ -> assert false
+    in
+    let proof_closer_id = match List.rev tasks with
+      | [] -> terminator_id
+      | (PSkip { id } | PExec { id } | PQuery { id }) :: _ -> id
+      | PDelegate _ :: _ -> assert false
+    in
+    let proof_begin_range = Document.range_of_id_with_blank_space document proof_opener_id in
+    let proof_end_range = Document.range_of_id_with_blank_space document proof_closer_id in
+    let range = Range.create ~end_:proof_end_range.end_ ~start:proof_begin_range.start in
+    log @@ "DELEGATED JOB RANGE: " ^ Range.to_string range;
+    log @@ "TRUNCATING FROM PREPARED";
+    (* When a job is delegated we shouldn't merge ranges (to get the proper progress report) *)
+    List.append processing [ range ], remove_or_truncate_range range prepared
   | PSkip { id } | PExec { id } | PQuery { id } ->
     let range = Document.range_of_id_with_blank_space document id in
+    log @@ "TRUNCATING FROM PREPARED";
     insert_or_merge_range range processing, remove_or_truncate_range range prepared
 
 let update_overview task todo state document overview =
-  let { processing; processed; prepared } = overview in
-  let processed, processing, prepared = update_processed task state processing processed prepared document in
+  let {processed; processing; prepared} = 
+  match task with 
+  | PDelegate { terminator_id } ->
+    let range = Document.range_of_id_with_blank_space document terminator_id in
+    update_processed_as_Done (Success None) range overview
+  | PSkip { id } | PExec { id } | PQuery { id } ->
+    update_processed id state document overview
+  in
   let processing, prepared = match todo with
   | [] -> processing, prepared
   | next :: _ -> update_processing next processing prepared document in
@@ -366,28 +378,29 @@ let handle_feedback id fb state =
 let handle_event event state =
   match event with
   | LocalFeedback (q,_,id,fb) ->
-      Some (handle_feedback id fb state), [local_feedback q]
+      None, Some (handle_feedback id fb state), [local_feedback q]
   | ProofWorkerEvent event ->
       let update, events = ProofWorker.handle_event event in
-      let state =
+      let state, id =
         match update with
-        | None -> None
+        | None -> None, None
         | Some (ProofJob.AppendFeedback(_,id,fb)) ->
-            Some (handle_feedback id fb state)
+            Some (handle_feedback id fb state), None
         | Some (ProofJob.UpdateExecStatus(id,v)) ->
             match SM.find id state.of_sentence, v with
             | (Delegated (_,completion), fl), _ ->
                 Option.default ignore completion v;
-                Some (update_all id (Done v) fl state)
+                Some (update_all id (Done v) fl state), Some id
             | (Done (Success s), fl), Error (err,_) ->
                 (* This only happens when a Qed closing a delegated proof
                    receives an updated by a worker saying that the proof is
                    not completed *)
-                Some (update_all id (Done (Error (err,s))) fl state)
-            | (Done _, _), _ -> None
-            | exception Not_found -> None (* TODO: is this possible? *)
+                Some (update_all id (Done (Error (err,s))) fl state), Some id
+            | (Done _, _), _ -> None, Some id
+            | exception Not_found -> None, None (* TODO: is this possible? *)
       in
-      inject_proof_events state events
+      let state, events = inject_proof_events state events in
+      id, state, events
 
 let find_fulfilled_opt x m =
   try
diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli
index 5e0741c3..dfacc167 100644
--- a/language-server/dm/executionManager.mli
+++ b/language-server/dm/executionManager.mli
@@ -66,7 +66,7 @@ val get_initial_context : state -> Evd.evar_map * Environ.env
 val get_vernac_state : state -> sentence_id -> Vernacstate.t option
 
 (** Events for the main loop *)
-val handle_event : event -> state -> (state option * events)
+val handle_event : event -> state -> (sentence_id option * state option * events)
 
 (** Execution happens in two steps. In particular the event one takes only
     one task at a time to ease checking for interruption *)
@@ -75,6 +75,7 @@ val build_tasks_for : Scheduler.schedule -> state -> sentence_id -> Vernacstate.
 val execute : state -> Vernacstate.t * events * bool -> prepared_task -> (state * Vernacstate.t * events * bool)
 
 val update_overview : prepared_task -> prepared_task list -> state -> Document.document -> exec_overview -> exec_overview
+val update_processed : sentence_id -> state -> Document.document -> exec_overview -> exec_overview
 
 (** Coq toplevels for delegation without fork *)
 module ProofWorkerProcess : sig