diff --git a/client/src/Decorations.ts b/client/src/Decorations.ts
index fa75f0d40..2a875043f 100644
--- a/client/src/Decorations.ts
+++ b/client/src/Decorations.ts
@@ -3,7 +3,7 @@ import * as vscode from 'vscode';
 import { DidChangeConfigurationParams } from 'vscode-languageclient';
 
 interface Decorations {
-  parsed: vscode.TextEditorDecorationType;
+  prepared: vscode.TextEditorDecorationType;
   processing: vscode.TextEditorDecorationType;
   processed: vscode.TextEditorDecorationType
 }
@@ -20,7 +20,7 @@ export function initializeDecorations(context: vscode.ExtensionContext) {
     }
 
     decorationsContinuous = {
-        parsed: create({
+        prepared: create({
             overviewRulerColor: 'cyan', 
             overviewRulerLane: vscode.OverviewRulerLane.Right,
         }),
@@ -35,7 +35,7 @@ export function initializeDecorations(context: vscode.ExtensionContext) {
     };
 
     decorationsManual = {
-        parsed: create({
+        prepared: create({
             outlineWidth: '1px',
             outlineStyle: 'solid', 
             overviewRulerColor: 'cyan', 
diff --git a/client/src/client.ts b/client/src/client.ts
index 9886f0cd5..8bbb06e7e 100644
--- a/client/src/client.ts
+++ b/client/src/client.ts
@@ -12,7 +12,9 @@ import {decorationsManual, decorationsContinuous} from './Decorations';
 export default class Client extends LanguageClient {
 
 	private static _channel: any = vscode.window.createOutputChannel('VsCoq');
-    private _decorations: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
+    private _decorationsPrepared: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
+    private _decorationsProcessed: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
+    private _decorationsProcessing: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
 
 	constructor(
         serverOptions: ServerOptions,
@@ -32,18 +34,26 @@ export default class Client extends LanguageClient {
         Client._channel.appendLine(message);
     }
 
-    public saveHighlights(uri: String, processingRange: vscode.Range[], processedRange: vscode.Range[]) {
-        this._decorations.set(uri, processedRange);
+    public saveHighlights(uri: String, preparedRange: vscode.Range[], processingRange: vscode.Range[], processedRange: vscode.Range[]) {
+        this._decorationsPrepared.set(uri, preparedRange);
+        this._decorationsProcessing.set(uri, processingRange);
+        this._decorationsProcessed.set(uri, processedRange);
     }
 
     public updateHightlights() {
-        for(let entry of this._decorations.entries()) {
+        for(let entry of this._decorationsPrepared.entries()) {
+            this.updateDocumentEditors(entry[0], entry[1], "prepared");
+        }
+        for(let entry of this._decorationsProcessing.entries()) {
+            this.updateDocumentEditors(entry[0], entry[1], "processing");
+        }
+        for(let entry of this._decorationsProcessed.entries()) {
             this.updateDocumentEditors(entry[0], entry[1]);
         }
     };
 
     public resetHighlights() {
-        for(let entry of this._decorations.entries()) {
+        for(let entry of this._decorationsProcessed.entries()) {
             this.resetDocumentEditors(entry[0]);
         }
     }
@@ -57,19 +67,39 @@ export default class Client extends LanguageClient {
     private resetDocumentEditors(uri: String) {
         const editors = this.getDocumentEditors(uri);
         editors.map(editor => {
+            editor.setDecorations(decorationsManual.prepared, []);
+            editor.setDecorations(decorationsContinuous.prepared, []);
+            editor.setDecorations(decorationsManual.processing, []);
+            editor.setDecorations(decorationsContinuous.processing, []);
             editor.setDecorations(decorationsManual.processed, []);
             editor.setDecorations(decorationsContinuous.processed, []);
         });
     }
 
-    private updateDocumentEditors(uri: String, ranges: vscode.Range[]) {
+    private updateDocumentEditors(uri: String, ranges: vscode.Range[], type: String = "processed") {
         const config = vscode.workspace.getConfiguration('vscoq.proof');
         const editors = this.getDocumentEditors(uri);
         editors.map(editor => {
             if(config.mode === 0) {
-                editor.setDecorations(decorationsManual.processed, ranges);
+                if(type === "prepared") {
+                    editor.setDecorations(decorationsManual.prepared, ranges);
+                }
+                if(type === "processing") {
+                    editor.setDecorations(decorationsManual.processing, ranges);
+                }
+                if (type === "processed") {
+                    editor.setDecorations(decorationsManual.processed, ranges);
+                }
             } else {
-                editor.setDecorations(decorationsContinuous.processed, ranges);
+                if(type === "prepared") {
+                    editor.setDecorations(decorationsContinuous.prepared, ranges);
+                }
+                if(type === "processing") {
+                    editor.setDecorations(decorationsContinuous.processing, ranges);
+                }
+                if (type === "processed") {
+                    editor.setDecorations(decorationsContinuous.processed, ranges);
+                }
             }
         });
     }
diff --git a/client/src/extension.ts b/client/src/extension.ts
index 2252a7d67..c1cf587bc 100644
--- a/client/src/extension.ts
+++ b/client/src/extension.ts
@@ -216,6 +216,7 @@ export function activate(context: ExtensionContext) {
         
             client.saveHighlights(
                 notification.uri,
+                notification.preparedRange,
                 notification.processingRange,
                 notification.processedRange
             );
diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts
index bc6045675..7475b00a3 100644
--- a/client/src/protocol/types.ts
+++ b/client/src/protocol/types.ts
@@ -59,7 +59,8 @@ export interface ProofViewNotification {
 }
 
 export interface UpdateHighlightsNotification {
-    uri: Uri; 
+    uri: Uri;
+    preparedRange: Range[];
     processingRange: Range[];
     processedRange: Range[];
 }
diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index 0ae008735..e8326f535 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -37,6 +37,7 @@ type state = {
   document : Document.document;
   execution_state : ExecutionManager.state;
   observe_id : observe_id option;
+  overview: exec_overview;
 }
 
 type event =
@@ -61,48 +62,76 @@ let inject_em_events events = List.map inject_em_event events
 
 type events = event Sel.Event.t list
 
-type exec_overview = {
-  processing : Range.t list;
-  processed : Range.t list;
-}
-
-let merge_adjacent_ranges (r1,l) r2 =
-  if Position.compare r1.Range.end_ r2.Range.start == 0 then
-    Range.{ start = r1.Range.start; end_ = r2.Range.end_ }, l
-  else
-    r2, r1 :: l
-
-let compress_sorted_ranges = function
-  | [] -> []
-  | range :: tl ->
-    let r, l = List.fold_left merge_adjacent_ranges (range,[]) tl in
-    r :: l
-
-let compress_ranges ranges =
-  let ranges = List.sort (fun { Range.start = s1 } { Range.start = s2 } -> Position.compare s1 s2) ranges in
-  compress_sorted_ranges ranges
-
-let executed_ranges doc execution_state loc =
-  let ranges_of l =
-    compress_ranges @@ List.map (Document.range_of_id_with_blank_space doc) l
-  in
-  let ids_before_loc = List.map (fun s -> s.Document.id) @@ Document.sentences_before doc loc in
-  let processed_ids = List.filter (fun x -> ExecutionManager.is_executed execution_state x || ExecutionManager.is_remotely_executed execution_state x) ids_before_loc in
-  log @@ Printf.sprintf "highlight: processed: %s" (String.concat " " (List.map Stateid.to_string processed_ids));
-  { 
-    processing = [];
-    processed = ranges_of processed_ids; 
-  }
+let print_exec_overview st =
+  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 @@ "-------------------------------------";
+  log @@ "--------- Processed ranges ---------";
+  List.iter (fun r -> log @@ Range.to_string r) processed;
+  log @@ "-------------------------------------"
+  
+let overview_until_range st range =
+  let find_final_range l = List.find_opt (fun (r: Range.t) -> Range.included ~in_:r range) l in
+  let {processed; processing; prepared} = st.overview in
+  let final_range = find_final_range processed  in
+  match final_range with
+  | None ->
+    let final_range = find_final_range processing in
+    begin match final_range with
+    | None -> { processed; processing; prepared }
+    | Some { start } ->
+      let processing = (List.filter (fun (r: Range.t) -> not @@ Range.included ~in_:r range) processing) in
+      let processing = List.append processing [Range.create ~start:start ~end_:range.end_] in
+      {processing; processed; prepared}
+    end
+  | Some { start } ->
+    let processed = (List.filter (fun (r: Range.t) -> not @@ Range.included ~in_:r range) processed) in
+    let processed = List.append processed [Range.create ~start:start ~end_:range.end_] in
+    { processing; processed; prepared }
+
+let prepare_overview st id =
+  match Document.get_sentence st.document id with
+  | None -> st (*Can't find the sentence, just return the state as is*)
+  | Some { id } ->
+    (* Sentence already executed, no need to prepare*)
+    if ExecutionManager.is_executed st.execution_state id then
+      st
+    else
+      (* Create the correct prepared range *)
+      begin match st.observe_id with
+      | None -> st (* No observe_id means continuous mode, no need to do anything*)
+      | Some Top ->
+        (* Create range from first sentence to id *)
+        let range = Document.range_of_id_with_blank_space st.document id in
+        let start = Position.create ~character:0 ~line:0 in
+        let range = Range.create ~end_: range.end_ ~start: start in
+        let prepared = [range] in
+        let overview = {st.overview with prepared} in
+        {st with overview}
+      | Some (Id o_id) ->
+        (* Create range from o_id to id*)
+        let o_range = Document.range_of_id_with_blank_space st.document o_id in
+        let range = Document.range_of_id_with_blank_space st.document id in
+        if Position.compare o_range.end_ range.end_ < 0 then
+          let range = Range.create ~end_: range.end_ ~start: o_range.end_ in
+          let prepared = [range] in
+          let overview = {st.overview with prepared} in
+          {st with overview}
+        else
+          st
+    end
 
 let executed_ranges st =
-  let loc = match st.observe_id with
-  | None -> max_int
-  | Some Top -> 0
-  | Some (Id id) -> match Document.get_sentence st.document id with 
-    | None -> failwith "observe_id does not exist"
-    | Some { stop } -> stop
-  in
-  executed_ranges st.document st.execution_state loc
+  match st.observe_id with
+  | None -> st.overview
+  | Some Top -> { processing = []; processed = []; prepared = []; }
+  | Some (Id id) ->
+      let range = Document.range_of_id st.document id in
+      overview_until_range st range
 
 let observe_id_range st = 
   let doc = Document.raw_document st.document in
@@ -177,13 +206,13 @@ let observe ~background state id : (state * event Sel.Event.t list) =
   match Document.get_sentence state.document id with
   | None -> (state, []) (* TODO error? *)
   | Some {id } ->
-    let vst_for_next_todo, todo = ExecutionManager.build_tasks_for (Document.schedule state.document) state.execution_state id in
+    let vst_for_next_todo, todo, _ = ExecutionManager.build_tasks_for (Document.schedule state.document) state.execution_state id in
     if CList.is_empty todo then
       (state, [])
     else
       let priority = if background then None else Some PriorityManager.execution in
       let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started = Unix.gettimeofday (); background }) in
-      (state, [ event ])
+      (state, [ event ] )
 
 let clear_observe_id st = 
   { st with observe_id = None }
@@ -192,6 +221,7 @@ let reset_to_top st =
   { st with observe_id = Some Top }
 
 let interpret_to st id =
+  let st = prepare_overview st id in
   let observe_id = if st.observe_id = None then None else (Some (Id id)) in
   let st = { st with observe_id} in
   observe ~background:false st id
@@ -291,7 +321,8 @@ let init init_vs ~opts uri ~text observe_id =
   let init_vs = Vernacstate.freeze_full_state () in
   let document = Document.create_document init_vs.Vernacstate.synterp text in
   let execution_state, feedback = ExecutionManager.init init_vs in
-  let st = { uri; opts; init_vs; document; execution_state; observe_id } in
+  let overview = { processing = []; processed = []; prepared = []} in
+  let st = { uri; opts; init_vs; document; execution_state; observe_id; overview } in
   validate_document st, [inject_em_event feedback]
 
 let reset { uri; opts; init_vs; document; execution_state; observe_id } =
@@ -301,7 +332,8 @@ let reset { uri; opts; init_vs; document; execution_state; observe_id } =
   ExecutionManager.destroy execution_state;
   let execution_state, feedback = ExecutionManager.init init_vs in
   let observe_id = if observe_id = None then None else (Some Top) in
-  let st = { uri; opts; init_vs; document; execution_state; observe_id} in
+  let overview = { processing = []; processed = []; prepared = []} in
+  let st = { uri; opts; init_vs; document; execution_state; observe_id; overview } in
   validate_document st, [inject_em_event feedback]
 
 let apply_text_edits state edits =
@@ -318,7 +350,7 @@ let apply_text_edits state edits =
 let handle_event ev st =
   match ev with
   | Execute { id; todo = []; started } -> (* the vst_for_next_todo is also in st.execution_state *)
-    let time = Unix.gettimeofday () -. started in 
+    let time = Unix.gettimeofday () -. started in
     log (Printf.sprintf "ExecuteToLoc %d ends after %2.3f" (Stateid.to_int id) time);
     (* We update the state to trigger a publication of diagnostics *)
     (Some st, [])
@@ -330,9 +362,20 @@ let handle_event ev st =
        executing *)
     let priority = if background then None else Some PriorityManager.execution in
     let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started; background }) in
-    (Some {st with execution_state}, inject_em_events events @ [event])
+    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/documentManager.mli b/language-server/dm/documentManager.mli
index 8466b3394..831312b38 100644
--- a/language-server/dm/documentManager.mli
+++ b/language-server/dm/documentManager.mli
@@ -33,6 +33,8 @@ val pp_event : Format.formatter -> event -> unit
 
 type events = event Sel.Event.t list
 
+val print_exec_overview : state -> unit
+
 val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> observe_id option -> state * events
 (** [init st opts uri text] initializes the document manager with initial vernac state
     [st] on which command line opts will be set. *)
@@ -78,11 +80,6 @@ val interpret_in_background : state -> (state * events)
 val reset : state -> state * events
 (** resets Coq *)
 
-type exec_overview = {
-  processing : Range.t list;
-  processed : Range.t list;
-}
-
 val executed_ranges : state -> exec_overview
 (** returns the ranges corresponding to the sentences
     that have been executed and remotely executes *)
diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 592ea452e..ef0d84905 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 open Protocol
+open Protocol.LspWrapper
 open Scheduler
 open Types
 
@@ -76,6 +77,7 @@ type state = {
   sel_cancellation_handle : Sel.Event.cancellation_handle;
 }
 
+
 let options = ref default_options
 
 let set_options o = options := o
@@ -228,6 +230,99 @@ let interp_qed_delayed ~proof_using ~state_id ~st =
   let st = { st with interp } in
   st, success st, assign
 
+let rec insert_or_merge_range r = function
+| [] -> [r]
+| r1 :: l ->
+  if Position.compare r1.Range.end_ r.Range.start == 0 then
+    Range.{ start = r1.Range.start; end_ = r.Range.end_ } :: l
+  else
+    r1 :: (insert_or_merge_range r l)
+
+let rec remove_or_truncate_range r = function
+| [] -> []
+| 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
+    l
+  else if Position.compare r1.Range.start r.Range.start == 0
+  then
+    Range.{ start = r.Range.end_; end_ = r1.Range.end_} :: l
+  else
+    r1 :: (remove_or_truncate_range r l)
+
+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
+  | 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; 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 {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
+  {processing; processed; prepared}
+
+
 let update_all id v fl state =
   { state with of_sentence = SM.add id (v, fl) state.of_sentence }
 ;;
@@ -283,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
@@ -476,29 +572,29 @@ let execute st (vs, events, interrupted) task =
       (st, vs, events, true)
 
 let build_tasks_for sch st id =
-  let rec build_tasks id tasks =
+  let rec build_tasks id tasks st =
     begin match find_fulfilled_opt id st.of_sentence with
     | Some (Success (Some vs)) ->
       (* We reached an already computed state *)
       log @@ "Reached computed state " ^ Stateid.to_string id;
-      vs, tasks
+      vs, tasks, st
     | Some (Error(_,Some vs)) ->
       (* We try to be resilient to an error *)
       log @@ "Error resiliency on state " ^ Stateid.to_string id;
-      vs, tasks
+      vs, tasks, st
     | _ ->
       log @@ "Non (locally) computed state " ^ Stateid.to_string id;
       let (base_id, task) = task_for_sentence sch id in
       begin match base_id with
       | None -> (* task should be executed in initial state *)
-        st.initial, task :: tasks
+        st.initial, task :: tasks, st
       | Some base_id ->
-        build_tasks base_id (task::tasks)
+        build_tasks base_id (task::tasks) st
       end
     end
   in
-  let vs, tasks = build_tasks id [] in
-  vs, List.concat_map prepare_task tasks
+  let vs, tasks, st = build_tasks id [] st in
+  vs, List.concat_map prepare_task tasks, st
 
 let all_errors st =
   List.fold_left (fun acc (id, (p,_)) ->
diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli
index ac38bab9c..dfacc167d 100644
--- a/language-server/dm/executionManager.mli
+++ b/language-server/dm/executionManager.mli
@@ -66,14 +66,17 @@ 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 *)
 type prepared_task
-val build_tasks_for : Scheduler.schedule -> state -> sentence_id -> Vernacstate.t * prepared_task list
+val build_tasks_for : Scheduler.schedule -> state -> sentence_id -> Vernacstate.t * prepared_task list * state
 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
   type options
diff --git a/language-server/dm/types.ml b/language-server/dm/types.ml
index 8ab99e161..e84d86a40 100644
--- a/language-server/dm/types.ml
+++ b/language-server/dm/types.ml
@@ -16,6 +16,12 @@ open Lsp.Types
 type sentence_id = Stateid.t
 type sentence_id_set = Stateid.Set.t
 
+type exec_overview = {
+  prepared: Range.t list;
+  processing : Range.t list;
+  processed : Range.t list;
+}
+
 type text_edit = Range.t * string
 
 type link = {
diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml
index c9ad09160..6a179c05d 100644
--- a/language-server/protocol/extProtocol.ml
+++ b/language-server/protocol/extProtocol.ml
@@ -84,16 +84,6 @@ module Notification = struct
 
   module Server = struct
 
-    module UpdateHighlightsParams = struct
-
-      type t = {
-        uri : DocumentUri.t;
-        processingRange : Range.t list;
-        processedRange : Range.t list;
-      } [@@deriving yojson]
-
-    end
-
     module MoveCursorParams = struct
       
       type t = {
@@ -114,7 +104,7 @@ module Notification = struct
 
     type t =
     | Std of Lsp.Server_notification.t
-    | UpdateHighlights of UpdateHighlightsParams.t
+    | UpdateHighlights of overview
     | MoveCursor of MoveCursorParams.t
     | ProofView of ProofViewParams.t
     | SearchResult of query_result
@@ -124,7 +114,7 @@ module Notification = struct
         Lsp.Server_notification.to_jsonrpc notification
       | UpdateHighlights params ->
         let method_ = "vscoq/updateHighlights" in
-        let params = UpdateHighlightsParams.yojson_of_t params in
+        let params = yojson_of_overview params in
         let params = Some (Jsonrpc.Structured.t_of_yojson params) in
         Jsonrpc.Notification.{ method_; params }
       | ProofView params -> 
diff --git a/language-server/protocol/lspWrapper.ml b/language-server/protocol/lspWrapper.ml
index 41ddb911a..d51d63d33 100644
--- a/language-server/protocol/lspWrapper.ml
+++ b/language-server/protocol/lspWrapper.ml
@@ -40,6 +40,8 @@ module Range = struct
     let (<=) x y = Position.compare x y <= 0 in
     in_.start <= start && end_ <= in_.end_
 
+  let to_string range = Format.sprintf ("Range (start: %s, end: %s)") (Position.to_string range.start) (Position.to_string range.end_)
+
 end 
 
 module DiagnosticSeverity = struct
@@ -62,5 +64,12 @@ type query_result =
     statement : pp;
   } [@@deriving yojson]
 
+type overview = {
+  uri : DocumentUri.t;
+  preparedRange: Range.t list;
+  processingRange : Range.t list;
+  processedRange : Range.t list;
+} [@@deriving yojson]
+
 type notification =
-  | QueryResultNotification of query_result
+  | QueryResultNotification of query_result
\ No newline at end of file
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index e0c4f59e8..8be949b73 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -180,10 +180,11 @@ let publish_diagnostics uri doc =
   output_notification (Std diag_notification)
 
 let send_highlights uri doc =
-  let { Dm.DocumentManager.processing;  processed } =
+  let { Dm.Types.processing;  processed; prepared } =
     Dm.DocumentManager.executed_ranges doc in
   let notification = Notification.Server.UpdateHighlights {
     uri;
+    preparedRange = prepared;
     processingRange = processing;
     processedRange = processed;
   }