diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index a21e44f5..bd573414 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -44,6 +44,13 @@ type state = {
   observe_id : observe_id option;
 }
 
+type parse_event = {
+  started: float;
+  state: state;
+  background: bool;
+  block_on_error: bool;
+}
+
 type event =
   | Execute of { (* we split the computation to help interruptibility *)
       id : Types.sentence_id; (* sentence of interest *)
@@ -55,11 +62,16 @@ type event =
       background: bool; (* Just to re-set execution priorities later down the loop *)
     }
   | ExecutionManagerEvent of ExecutionManager.event
+  | ParseEvent of parse_event
+
 let pp_event fmt = function
   | Execute { id; todo; started; _ } ->
       let time = Unix.gettimeofday () -. started in 
       Stdlib.Format.fprintf fmt "ExecuteToLoc %d (%d tasks left, started %2.3f ago)" (Stateid.to_int id) (List.length todo) time
   | ExecutionManagerEvent _ -> Stdlib.Format.fprintf fmt "ExecutionManagerEvent"
+  | ParseEvent { started; _} -> 
+    let time = Unix.gettimeofday () -. started in 
+    Stdlib.Format.fprintf fmt "ParseEvent (started %2.3f ago)" time
 
 let inject_em_event x = Sel.Event.map (fun e -> ExecutionManagerEvent e) x
 let inject_em_events events = List.map inject_em_event events
@@ -435,7 +447,7 @@ let dirpath_of_top = Coqargs.dirpath_of_top
 let dirpath_of_top = Coqinit.dirpath_of_top
 [%%endif]
 
-let init init_vs ~opts uri ~text observe_id =
+let init init_vs ~opts uri ~text ~background ~block_on_error observe_id =
   Vernacstate.unfreeze_full_state init_vs;
   let top = try (dirpath_of_top (TopPhysical (DocumentUri.to_path uri))) with
     e -> raise e
@@ -444,20 +456,26 @@ 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
-  validate_document st, [inject_em_event feedback]
+  let state = { uri; opts; init_vs; document; execution_state; observe_id } in
+  let started = Unix.gettimeofday () in
+  let priority = Some PriorityManager.parsing in
+  let event = [Sel.now ?priority (ParseEvent {started; state; background; block_on_error})] in
+  state, event @ [inject_em_event feedback]
 
-let reset { uri; opts; init_vs; document; execution_state; observe_id } =
+let reset { uri; opts; init_vs; document; execution_state; observe_id } ~background ~block_on_error =
   let text = RawDocument.text @@ Document.raw_document document in
   Vernacstate.unfreeze_full_state init_vs;
   let document = Document.create_document init_vs.synterp text in
   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
-  validate_document st, [inject_em_event feedback]
+  let state = { uri; opts; init_vs; document; execution_state; observe_id } in
+  let started = Unix.gettimeofday () in
+  let priority = Some PriorityManager.parsing in
+  let event = [Sel.now ?priority (ParseEvent {started; state; background; block_on_error})] in
+  state, event @ [inject_em_event feedback]
 
-let apply_text_edits state edits =
+let apply_text_edits state edits ~background ~block_on_error =
   let apply_edit_and_shift_diagnostics_locs_and_overview state (range, new_text as edit) =
     let document = Document.apply_text_edit state.document edit in
     let exec_st = state.execution_state in
@@ -470,7 +488,9 @@ let apply_text_edits state edits =
     {state with execution_state; document}
   in
   let state = List.fold_left apply_edit_and_shift_diagnostics_locs_and_overview state edits in
-  validate_document state
+  let priority = Some PriorityManager.parsing in
+  let started = Unix.gettimeofday () in
+  [Sel.now ?priority (ParseEvent {started; state; background; block_on_error})]
 
 let execution_finished st id started =
   let time = Unix.gettimeofday () -. started in
@@ -540,6 +560,21 @@ let handle_execution_manager_event st ev =
   in
   (st, inject_em_events events, None)
 
+let rec most_recent_parsing_event acc = function
+  | [] -> acc
+  | ParseEvent { started } :: rest -> most_recent_parsing_event (Float.max acc started) rest
+  | _ :: rest -> most_recent_parsing_event acc rest
+
+let prune_outdated el =
+  (* remove old parsing events *)
+  let ts = most_recent_parsing_event 0.0 el in
+  let most_recent_pe = function
+      | ParseEvent {started; } -> Float.equal ts started
+      | _ -> true in
+  let el = List.filter most_recent_pe el in
+  (* TODO: filter old exec events *)
+  el
+
 let handle_event ev st block =
   match ev with
   | Execute { id; todo = []; started } -> (* the vst_for_next_todo is also in st.execution_state *)
@@ -548,7 +583,29 @@ let handle_event ev st block =
     execute st id vst_for_next_todo started task todo background block
   | ExecutionManagerEvent ev ->
     handle_execution_manager_event st ev
-
+  | ParseEvent { state; background; block_on_error } ->
+    let st = validate_document state in
+    if background then
+      let (st, events, blocking_error) = interpret_in_background st ~should_block_on_error:block_on_error in
+      (Some st), events, blocking_error
+    else
+      (Some st), [], None
+
+
+let handle_events el st0 block =
+  let el = prune_outdated el in
+  let rec handle st new_events el =
+    match el with
+    | [] -> st, [], None
+    | e :: el ->
+        let st = Option.default st0 st in
+        let st, more_new_events, stop = handle_event e st block in
+        let new_events = new_events @ more_new_events in
+        if Option.is_empty stop then handle st new_events el
+        else st, new_events, stop (* BUG: do something with el *)
+  in
+    handle None [] el 
+      
 let get_proof st diff_mode pos =
   let previous_st id =
     let oid = fst @@ Scheduler.task_for_sentence (Document.schedule st.document) id in
diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli
index 179d0f5d..1d99740b 100644
--- a/language-server/dm/documentManager.mli
+++ b/language-server/dm/documentManager.mli
@@ -38,14 +38,17 @@ val pp_event : Format.formatter -> event -> unit
 
 type events = event Sel.Event.t list
 
-val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> observe_id option -> state * events
+val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> background:bool -> block_on_error:bool -> 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. *)
+    [st] on which command line opts will be set. [background] indicates if the document should
+    be executed in the background once it is parsed. *)
 
-val apply_text_edits : state -> text_edit list -> state
-(** [apply_text_edits doc edits] updates the text of [doc] with [edits]. The new
+val apply_text_edits : state -> text_edit list -> background:bool -> block_on_error:bool -> events
+(** [apply_text_edits doc edits] updates the text of [doc] with [edits]. 
+    A ParseEvent is triggered, once processed: the new
     document is parsed, outdated executions states are invalidated, and the observe
-    id is updated. *)
+    id is updated. Finally if [background] is set to true, an execution is launched in
+    the background *)
 
 val clear_observe_id : state -> state
 (** [clear_observe_id state] updates the state to make the observe_id None *)
@@ -83,7 +86,7 @@ val interpret_in_background : state -> should_block_on_error:bool -> (state * ev
 (** [interpret_in_background doc] same as [interpret_to_end] but computation 
     is done in background (with lower priority) *)
 
-val reset : state -> state * events
+val reset : state -> background:bool -> block_on_error:bool -> state * events
 (** resets Coq *)
 
 val executed_ranges : state -> exec_overview
@@ -109,7 +112,7 @@ val get_proof : state -> Settings.Goals.Diff.Mode.t -> Position.t option -> Proo
 
 val get_completions : state -> Position.t -> (completion_item list, string) Result.t
 
-val handle_event : event -> state -> bool -> (state option * events * blocking_error option)
+val handle_events : event list -> state -> bool -> (state option * events * blocking_error option)
 (** handles events and returns a new state if it was updated *)
 
 val search : state -> id:string -> Position.t -> string -> notification Sel.Event.t list
diff --git a/language-server/dm/priorityManager.ml b/language-server/dm/priorityManager.ml
index e07c7719..17b55c87 100644
--- a/language-server/dm/priorityManager.ml
+++ b/language-server/dm/priorityManager.ml
@@ -1,7 +1,8 @@
 (* This filecontains the global views of priorities *)
 
-let lsp_message = -3
-let feedback = -4
+let lsp_message = -5
+let feedback = -6
+let parsing = -4
 let execution = -3
 let proof_view = -2
-let move_cursor = -5
\ No newline at end of file
+let move_cursor = -7
\ No newline at end of file
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index d9e4f4d4..a2c773f5 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -58,14 +58,38 @@ type lsp_event =
   | Receive of Jsonrpc.Packet.t option
   | Send of Jsonrpc.Packet.t
 
+type timestamp = float
+
+type my_event =
+  | LspManagerEvent of lsp_event
+  | Notification of notification
+  | SendProofView of DocumentUri.t * Position.t option
+  | SendMoveCursor of DocumentUri.t * Range.t
+  | SendBlockOnError of DocumentUri.t * Range.t
+  | LogEvent of Dm.Log.event
+
 type event =
- | LspManagerEvent of lsp_event
- | DocumentManagerEvent of DocumentUri.t * Dm.DocumentManager.event
- | Notification of notification
- | LogEvent of Dm.Log.event
- | SendProofView of DocumentUri.t * Position.t option
- | SendMoveCursor of DocumentUri.t * Range.t
- | SendBlockOnError of DocumentUri.t * Range.t
+  | DocumentManagerEvent of DocumentUri.t * Dm.DocumentManager.event
+  | MyEvent of my_event
+
+module UriMap = struct
+  include Map.Make(DocumentUri)
+  let append k v t =
+    try let l = find k t in add k (l @ [v]) t
+    with Not_found -> add k [v] t
+end
+
+type events_by_component = {
+  lsp_events : my_event list;
+  dm_events : Dm.DocumentManager.event list UriMap.t;
+}
+let partition_events_by_component l =
+  let rec aux us dm = function
+    | [] -> { lsp_events = List.rev us; dm_events = dm }
+    | DocumentManagerEvent(uri,e) :: rest -> aux us (UriMap.append uri e dm) rest
+    | MyEvent e :: rest -> aux (e :: us) dm rest
+in
+  aux [] UriMap.empty l
 
 type events = event Sel.Event.t list
 
@@ -74,10 +98,10 @@ let lsp : event Sel.Event.t =
     | Ok buff ->
       begin
         log "UI req ready";
-        try LspManagerEvent (Receive (Some (Jsonrpc.Packet.t_of_yojson (Yojson.Safe.from_string (Bytes.to_string buff)))))
+        try MyEvent (LspManagerEvent (Receive (Some (Jsonrpc.Packet.t_of_yojson (Yojson.Safe.from_string (Bytes.to_string buff))))))
         with exn ->
           log @@ "failed to decode json";
-          LspManagerEvent (Receive None)
+          MyEvent (LspManagerEvent (Receive None))
       end
     | Error exn ->
         log @@ ("failed to read message: " ^ Printexc.to_string exn);
@@ -96,13 +120,14 @@ let output_notification notif =
   output_json @@ Jsonrpc.Notification.yojson_of_t @@ Notification.Server.to_jsonrpc notif
 
 let inject_dm_event uri x : event Sel.Event.t =
+  (* let time = Unix.gettimeofday () in *)
   Sel.Event.map (fun e -> DocumentManagerEvent(uri,e)) x
 
 let inject_notification x : event Sel.Event.t =
-  Sel.Event.map (fun x -> Notification(x)) x
+  Sel.Event.map (fun x -> MyEvent (Notification(x))) x
 
 let inject_debug_event x : event Sel.Event.t =
-  Sel.Event.map (fun x -> LogEvent x) x
+  Sel.Event.map (fun x -> MyEvent (LogEvent x)) x
 
 let inject_dm_events (uri,l) =
   List.map (inject_dm_event uri) l
@@ -168,7 +193,7 @@ let do_initialize id params =
   } in
   log "---------------- initialized --------------";
   let debug_events = Dm.Log.lsp_initialization_done () |> inject_debug_events in
-  Ok initialize_result, debug_events@[Sel.now @@ LspManagerEvent (send_configuration_request ())]
+  Ok initialize_result, debug_events@[Sel.now @@ MyEvent (LspManagerEvent (send_configuration_request ()))]
 
 let do_shutdown id params =
   Ok(()), []
@@ -259,19 +284,12 @@ let reset_observe_ids =
 let open_new_document uri text =
   let vst, opts = get_init_state () in
   let observe_id = if !check_mode = Settings.Mode.Continuous then None else Some Dm.DocumentManager.Top in
-  let st, events = try Dm.DocumentManager.init vst ~opts uri ~text observe_id with
+  let st, events = try Dm.DocumentManager.init vst ~opts uri ~text ~background:(!check_mode = Settings.Mode.Continuous) ~block_on_error:!block_on_first_error observe_id with
     e -> raise e
   in
-  let (st, events') = 
-    if !check_mode = Settings.Mode.Continuous then
-      let (st, events, _) = Dm.DocumentManager.interpret_in_background st ~should_block_on_error:!block_on_first_error in
-      (st, events)
-    else 
-      (st, [])
-  in
   Hashtbl.add states (DocumentUri.to_path uri) { st ; visible = true };
   update_view uri st;
-  inject_dm_events (uri, events@events')
+  inject_dm_events (uri, events)
 
 let textDocumentDidOpen params =
   let Lsp.Types.DidOpenTextDocumentParams.{ textDocument = { uri; text } } = params in
@@ -298,14 +316,7 @@ let textDocumentDidChange params =
         Option.get range, text
       in
       let text_edits = List.map mk_text_edit contentChanges in
-      let st = Dm.DocumentManager.apply_text_edits st text_edits in
-      let (st, events) = 
-        if !check_mode = Settings.Mode.Continuous then
-          let (st, events, _) = Dm.DocumentManager.interpret_in_background st ~should_block_on_error:!block_on_first_error in
-          (st, events)
-        else 
-          (st, [])
-      in
+      let events = Dm.DocumentManager.apply_text_edits st text_edits ~background:(!check_mode = Settings.Mode.Continuous) ~block_on_error:!block_on_first_error in
       replace_state (DocumentUri.to_path uri) st visible;
       update_view uri st;
       inject_dm_events (uri, events)
@@ -364,20 +375,20 @@ let progress_hook uri () =
   | Some { st } -> update_view uri st
 
 let mk_proof_view_event uri position = 
-  Sel.now ~priority:Dm.PriorityManager.proof_view (SendProofView (uri, position))
+  Sel.now ~priority:Dm.PriorityManager.proof_view (MyEvent (SendProofView (uri, position)))
 
 let mk_move_cursor_event uri range = 
   let priority = Dm.PriorityManager.move_cursor in
-  Sel.now ~priority @@ SendMoveCursor (uri, range)
+  Sel.now ~priority @@ MyEvent (SendMoveCursor (uri, range))
 
 let mk_block_on_error_event_no_move uri error_range =
   let priority = Dm.PriorityManager.move_cursor in
-  let event = Sel.now ~priority @@ SendBlockOnError (uri, error_range) in
+  let event = Sel.now ~priority @@ MyEvent (SendBlockOnError (uri, error_range)) in
   [event] @ [mk_proof_view_event uri (Some error_range.end_)]
 
 let mk_block_on_error_event uri last_range error_range =
   let priority = Dm.PriorityManager.move_cursor in
-  let event = Sel.now ~priority @@ SendBlockOnError (uri, error_range) in
+  let event = Sel.now ~priority @@ MyEvent (SendBlockOnError (uri, error_range)) in
   [event] @ [mk_move_cursor_event uri last_range] @ [mk_proof_view_event uri (Some error_range.end_)]
 
 
@@ -496,17 +507,10 @@ let coqtopResetCoq id params =
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log @@ "[resetCoq] ignoring event on non existent document"; Error("Document does not exist"), []
   | Some { st; visible } -> 
-    let st, events = Dm.DocumentManager.reset st in
-    let (st, events') =
-      if !check_mode = Settings.Mode.Continuous then
-        let (st, events, _) = Dm.DocumentManager.interpret_in_background st ~should_block_on_error:!block_on_first_error in
-        (st, events)
-      else
-        (st, [])
-    in
+    let st, events = Dm.DocumentManager.reset st ~background:(!check_mode = Settings.Mode.Continuous) ~block_on_error:!block_on_first_error in
     replace_state (DocumentUri.to_path uri) st visible;
     update_view uri st;
-    Ok(()), (uri,events@events') |> inject_dm_events
+    Ok(()), (uri,events) |> inject_dm_events
 
 let coqtopInterpretToEnd params =
   let Notification.Client.InterpretToEndParams.{ textDocument = { uri } } = params in
@@ -679,15 +683,14 @@ let output_notification = function
 | QueryResultNotification params ->
   output_notification @@ SearchResult params
 
-let handle_event = function
-  | LspManagerEvent e -> handle_lsp_event e
-  | DocumentManagerEvent (uri, e) ->
+
+let handle_dm_events_for_one_uri uri el new_events =
     begin match Hashtbl.find_opt states (DocumentUri.to_path uri) with
     | None ->
       log @@ "ignoring event on non-existing document";
       []
     | Some { st; visible } ->
-      let (ost, events, error_range) = Dm.DocumentManager.handle_event e st !block_on_first_error in
+      let (ost, events, error_range) = Dm.DocumentManager.handle_events el st !block_on_first_error in
       begin match ost with
         | None -> ()
         | Some st ->
@@ -703,6 +706,13 @@ let handle_event = function
         else
           inject_dm_events (uri, events)
     end
+    :: new_events
+
+let handle_dm_events m =
+  UriMap.fold handle_dm_events_for_one_uri m [] |> List.concat
+
+let handle_my_event = function
+  | LspManagerEvent e -> handle_lsp_event e
   | Notification notification ->
     begin match notification with 
     | QueryResultNotification _ -> 
@@ -727,15 +737,26 @@ let handle_event = function
   | SendBlockOnError (uri, range) ->
     send_block_on_error uri range; []
 
-let pr_event = function
+let handle_my_events l = List.concat_map handle_my_event l
+
+let handle_events l =
+  let { dm_events; lsp_events } = partition_events_by_component l in
+  let new_dm_events = handle_dm_events dm_events in
+  let new_lsp_events = handle_my_events lsp_events in
+  new_lsp_events @ new_dm_events
+
+let pr_my_event = function
   | LspManagerEvent e -> pr_lsp_event e
-  | DocumentManagerEvent (uri, e) ->
-    Pp.str @@ Format.asprintf "%a" Dm.DocumentManager.pp_event e
   | Notification _ -> Pp.str"notif"
-  | LogEvent _ -> Pp.str"debug"
   | SendProofView _ -> Pp.str"proofview"
   | SendMoveCursor _ -> Pp.str"move cursor"
   | SendBlockOnError _ -> Pp.str"block on error"
+  | LogEvent _ -> Pp.str"debug"
+
+let pr_event = function
+  | DocumentManagerEvent (uri, e) ->
+    Pp.str @@ Format.asprintf "%a" Dm.DocumentManager.pp_event e
+  | MyEvent e -> pr_my_event e
 
 let init injections =
   init_state := Some (Vernacstate.freeze_full_state (), injections);
diff --git a/language-server/vscoqtop/lspManager.mli b/language-server/vscoqtop/lspManager.mli
index 5aed1f35..75a39018 100644
--- a/language-server/vscoqtop/lspManager.mli
+++ b/language-server/vscoqtop/lspManager.mli
@@ -15,7 +15,7 @@
 type event
 type events = event Sel.Event.t list
 
-val handle_event : event -> events
+val handle_events : event list -> events
 val pr_event : event -> Pp.t
 
 val init : Coqargs.injection_command list -> event Sel.Event.t list
\ No newline at end of file
diff --git a/language-server/vscoqtop/vscoqtop.ml b/language-server/vscoqtop/vscoqtop.ml
index 53476295..7163e4d9 100644
--- a/language-server/vscoqtop/vscoqtop.ml
+++ b/language-server/vscoqtop/vscoqtop.ml
@@ -22,10 +22,10 @@ let loop injections =
   let rec loop (todo : LspManager.event Sel.Todo.t) =
     (*log @@ "looking for next step";*)
     flush_all ();
-    let ready, todo = Sel.pop todo in
+    let events, todo = Sel.wait todo in
     let nremaining = Sel.Todo.size todo in
-    log @@ "Main loop event ready: " ^ Pp.string_of_ppcmds (LspManager.pr_event ready) ^ " , " ^ string_of_int nremaining ^ " events waiting";
-    let new_events = LspManager.handle_event ready in
+    log @@ "Main loop event ready: " ^ Pp.string_of_ppcmds (Pp.prlist LspManager.pr_event events) ^ " , " ^ string_of_int nremaining ^ " events waiting";
+    let new_events = LspManager.handle_events events in
     let todo = Sel.Todo.add todo new_events in
     loop todo
   in