diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index 1350bd14c..d2f362f07 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -56,6 +56,7 @@ type event =
   | Observe of Types.sentence_id
   | ParseMore of Document.event
   | SendProofView of Types.sentence_id
+  | SendBlockOnError of Types.sentence_id
 
 type handled_event = {
     state : state option;
@@ -77,6 +78,9 @@ let pp_event fmt = function
   | ParseMore _ -> Stdlib.Format.fprintf fmt "ParseMore event"
   | SendProofView id ->
     Stdlib.Format.fprintf fmt "SendProofView %d" @@ (Stateid.to_int id)
+  | SendBlockOnError id ->
+    Stdlib.Format.fprintf fmt "SendBlockOnError %d" @@ (Stateid.to_int id)
+
 let inject_em_event x = Sel.Event.map (fun e -> ExecutionManagerEvent e) x
 let inject_em_events events = List.map inject_em_event events
 let inject_doc_event x = Sel.Event.map (fun e -> ParseMore e) x
@@ -570,6 +574,13 @@ let handle_event ev st block background diff_mode =
     let notification = Some (Notification.Server.ProofView params) in
     let update_view = true in
     {state=(Some st); events=[]; update_view; blocking_error=None; notification}
+  | SendBlockOnError id ->
+    let {uri} = st in
+    let range = Document.range_of_id st.document id in
+    let notification = Some (Notification.Server.BlockOnError {uri; range}) in
+    {state=(Some st); events=[]; blocking_error=None; update_view=false; notification}
+
+
 
 let context_of_id st = function
   | None -> Some (ExecutionManager.get_initial_context st.execution_state)
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index b7cfd33fa..44279f753 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -300,7 +300,7 @@ let open_new_document uri text =
   in
 
   let vst = init_document local_args vst in
-  let st, events = try Dm.DocumentManager.init vst ~opts uri ~text with
+  let st, events = try Dm.DocumentManager.init vst ~opts:(Coqargs.injection_commands local_args) uri ~text with
     e -> raise e
   in
   Hashtbl.add states (DocumentUri.to_path uri) { st ; visible = true; };
@@ -414,48 +414,21 @@ let coqtopInterpretToPoint params =
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log @@ "[interpretToPoint] ignoring event on non existent document"; []
   | Some { st; visible } ->
-    let (st, events, error_range, position) =
-      match !point_interp_mode with
-      | Settings.PointInterpretationMode.Cursor ->
-        let st, evs, blocking_err = Dm.DocumentManager.interpret_to_position st position in
-        (st, evs, blocking_err, position)
-      | Settings.PointInterpretationMode.NextCommand ->
-        Dm.DocumentManager.interpret_to_next_position st position
+    let (st, events, error_range) = Dm.DocumentManager.interpret_to_position st position ~check_mode:!check_mode ~point_interp_mode:!point_interp_mode
     in
     replace_state (DocumentUri.to_path uri) st visible;
     update_view uri st;
     let sel_events = inject_dm_events (uri, events) in
-    match error_range with
-    | None ->
-      sel_events @ [ mk_proof_view_event uri (Some position)]
-    | Some {last_range; error_range} ->
-      if !check_mode = Settings.Mode.Manual then
-        sel_events @ mk_block_on_error_event uri last_range error_range
-      else
-        sel_events @ [mk_proof_view_event uri (Some error_range.end_)]
+    sel_events
  
 let coqtopStepBackward params =
   let Notification.Client.StepBackwardParams.{ textDocument = { uri }; position } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log "[stepBackward] ignoring event on non existent document"; []
   | Some { st; visible } ->
-    if !check_mode = Settings.Mode.Continuous then
-      match position with
-      | None -> []
-      | Some pos -> 
-        match Dm.DocumentManager.get_previous_range st pos with
-        | None -> []
-        | Some range -> [mk_move_cursor_event uri range]
-    else
-      let (st, events, _) = Dm.DocumentManager.interpret_to_previous st in
-      let range = Dm.DocumentManager.observe_id_range st in
+      let (st, events, _) = Dm.DocumentManager.interpret_to_previous st ~check_mode:!check_mode in
       replace_state (DocumentUri.to_path uri) st visible;
-      update_view uri st;
-      match range with
-      | None ->
-        inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
-      | Some range ->
-        [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
+      inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
 
 let coqtopStepForward params =
   let Notification.Client.StepForwardParams.{ textDocument = { uri }; position } = params in
@@ -470,14 +443,10 @@ let coqtopStepForward params =
         | None -> []
         | Some range -> [mk_move_cursor_event uri range]
     else
-      let (st, events, error_range) = Dm.DocumentManager.interpret_to_next st in
-      let range = Dm.DocumentManager.observe_id_range st in
+      let (st, events, error_range) = Dm.DocumentManager.interpret_to_next st ~check_mode:!check_mode in
       replace_state (DocumentUri.to_path uri) st visible;
       update_view uri st;
-      match range, error_range with
-        | None, None -> inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
-        | _, Some { last_range; error_range} -> inject_dm_events (uri,events) @ mk_block_on_error_event_no_move uri error_range
-        | Some range, None -> [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
+      inject_dm_events (uri,events) 
         
   
   let make_CompletionItem i item : CompletionItem.t = 
@@ -533,14 +502,10 @@ let coqtopInterpretToEnd params =
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log @@ "[interpretToEnd] ignoring event on non existent document"; []
   | Some { st; visible } ->
-    let (st, events, error_range) = Dm.DocumentManager.interpret_to_end st in
+    let (st, events, error_range) = Dm.DocumentManager.interpret_to_end st ~check_mode:!check_mode in
     replace_state (DocumentUri.to_path uri) st visible;
     update_view uri st;
-    match error_range with
-    | None ->
-      inject_dm_events (uri,events) @ [ mk_proof_view_event uri None]
-    | Some {last_range; error_range} ->
-      inject_dm_events (uri,events) @ mk_block_on_error_event uri last_range error_range
+    inject_dm_events (uri,events)
 
 let coqtopLocate id params = 
   let Request.Client.LocateParams.{ textDocument = { uri }; position; pattern } = params in
@@ -735,14 +700,7 @@ let handle_event = function
   | SendProofView (uri, position) -> 
     begin match Hashtbl.find_opt states (DocumentUri.to_path uri) with
     | None -> log @@ "ignoring event on non existent document"; []
-    | Some { st } ->
-      let proof = Dm.DocumentManager.get_proof st !diff_mode position in
-      let messages = Dm.DocumentManager.get_messages st position in
-      let messages =
-        if !full_messages then messages
-        else List.filter (fun (sev,_) -> sev == DiagnosticSeverity.Information) messages
-      in
-      send_proof_view Notification.Server.ProofViewParams.{ proof; messages }; []
+    | Some { st } -> []
     end
   | SendMoveCursor (uri, range) -> 
     send_move_cursor uri range; []