diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml
index 1a2634af1..6d0e8caf9 100644
--- a/language-server/dm/document.ml
+++ b/language-server/dm/document.ml
@@ -107,6 +107,13 @@ type parse_state = {
   previous_document: document;
 }
 
+type parsing_end_info = {
+    unchanged_id: sentence_id option;
+    invalid_ids: sentence_id_set;
+    previous_document: document;
+    parsed_document: document;
+}
+
 type event = 
 | ParseEvent of parse_state
 | Invalidate of parse_state
@@ -615,7 +622,8 @@ let handle_invalidate {parsed; errors; parsed_comments; stop; top_id; started; p
     List.fold_left (fun acc (comment : comment) -> LM.add comment.stop comment acc) comments new_comments
   in
   let parsed_loc = pos_at_end document in
-  Some (unchanged_id, invalid_ids, previous_document, { document with parsed_loc; parsing_errors_by_end; comments_by_end})
+  let parsed_document = {document with parsed_loc; parsing_errors_by_end; comments_by_end} in
+  Some {parsed_document; unchanged_id; invalid_ids; previous_document}
 
 let handle_event document = function
 | ParseEvent state -> 
diff --git a/language-server/dm/document.mli b/language-server/dm/document.mli
index ffb0b961f..03cbc3052 100644
--- a/language-server/dm/document.mli
+++ b/language-server/dm/document.mli
@@ -37,6 +37,14 @@ type outline_element = {
 
 type outline = outline_element list
 
+
+type parsing_end_info = {
+    unchanged_id: sentence_id option;
+    invalid_ids: sentence_id_set;
+    previous_document: document;
+    parsed_document: document;
+}
+
 type event
 val pp_event : Format.formatter -> event -> unit
 
@@ -54,7 +62,7 @@ val validate_document : document -> document * events
 (** [validate_document doc] triggers the parsing of the document line by line without
     launching any execution. *)
 
-val handle_event : document -> event -> document * events * (sentence_id option * sentence_id_set * document * document) option
+val handle_event : document -> event -> document * events * parsing_end_info option
 (** [handle_event dpc ev] handles a parsing event for the document. One parsing event parses one line
     and prepares the next parsing event. Finally once the full parsing is done, the final event returs
     the id of the bottomost sentence of the prefix which has not changed since the previous validation
diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index b30559777..79419641d 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -428,18 +428,18 @@ let is_above st id1 id2 =
   let range2 = Document.range_of_id st id2 in
   Position.compare range1.start range2.start < 0
 
-let validate_document state unchanged_id invalid_roots prev_document new_document =
-  let state = {state with document=new_document} in
+let validate_document state (Document.{unchanged_id; invalid_ids; previous_document; parsed_document}) =
+  let state = {state with document=parsed_document} in
   let observe_id = match unchanged_id, state.observe_id with
     | None, Id _ -> Top
     | _, Top -> Top
-    | Some id, Id id' -> if is_above prev_document id id' then (Id id) else state.observe_id
+    | Some id, Id id' -> if is_above previous_document id id' then (Id id) else state.observe_id
   in
   let execution_state =
     List.fold_left (fun st id ->
-      ExecutionManager.invalidate prev_document (Document.schedule prev_document) id st
-      ) state.execution_state (Stateid.Set.elements invalid_roots) in
-  let execution_state = ExecutionManager.reset_overview execution_state prev_document in
+      ExecutionManager.invalidate previous_document (Document.schedule previous_document) id st
+      ) state.execution_state (Stateid.Set.elements invalid_ids) in
+  let execution_state = ExecutionManager.reset_overview execution_state previous_document in
   { state with  execution_state; observe_id }
 
 [%%if coq = "8.18" || coq = "8.19"]
@@ -577,15 +577,15 @@ let handle_event ev st ~block check_mode diff_mode =
     let events = inject_doc_events events in
     {state; events; update_view; notification=None}
   | ParseMore ev ->
-    let document, events, update = Document.handle_event st.document ev in
-    begin match update with
+    let document, events, parsing_end_info = Document.handle_event st.document ev in
+    begin match parsing_end_info with
     | None ->
       let update_view = false in
       let state = Some {st with document} in
       let events = inject_doc_events events in
       {state; events; update_view; notification=None}
-    | Some (unchanged_id, invalid_roots, prev_document, new_document) ->
-      let st = validate_document st unchanged_id invalid_roots prev_document new_document in
+    | Some parsing_end_info ->
+      let st = validate_document st parsing_end_info in
       let update_view = true in
       if check_mode = Settings.Mode.Continuous then
         let (st, events) = interpret_to_end st check_mode in
@@ -796,7 +796,7 @@ module Internal = struct
     | Top -> None
     | (Id id) -> Some id
 
-  let validate_document st (a,b,c,d) = validate_document st a b c d
+  let validate_document st parsing_end_info = validate_document st parsing_end_info
 
   let string_of_state st =
     let code_lines_by_id = Document.code_lines_sorted_by_loc st.document in
diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli
index 75c28ecf3..195ed6e23 100644
--- a/language-server/dm/documentManager.mli
+++ b/language-server/dm/documentManager.mli
@@ -142,7 +142,7 @@ module Internal : sig
   val observe_id : state -> sentence_id option
   val inject_doc_events : Document.event Sel.Event.t list -> event Sel.Event.t list
 
-  val validate_document : state -> sentence_id option * sentence_id_set * Document.document * Document.document -> state
+  val validate_document : state -> Document.parsing_end_info -> state
 
 
 end
diff --git a/language-server/tests/common.ml b/language-server/tests/common.ml
index c4cc92164..4ab84e8be 100644
--- a/language-server/tests/common.ml
+++ b/language-server/tests/common.ml
@@ -146,7 +146,7 @@ let rec handle_dm_events n (events : DocumentManager.event Sel.Todo.t) st =
     | Some ev ->
       (* Stdlib.Format.eprintf "handle_dm_events: handling %a\n"  DocumentManager.pp_event ev; *)
       let st, new_events =
-        match DocumentManager.handle_event ev st ~block:false ~background:false Protocol.Settings.Goals.Diff.Mode.Off with
+        match DocumentManager.handle_event ev st ~block:false Protocol.Settings.Mode.Manual Protocol.Settings.Goals.Diff.Mode.Off with
         | { DocumentManager.state = None; events = events' } -> st, events'
         | { DocumentManager.state = Some st; events = events' } -> st, events'
       in
@@ -155,7 +155,7 @@ let rec handle_dm_events n (events : DocumentManager.event Sel.Todo.t) st =
   end
  
 
-let rec handle_d_events n (events : Document.event Sel.Todo.t) (st : Document.document) :  sentence_id option * sentence_id_set * Document.document * Document.document =
+let rec handle_d_events n (events : Document.event Sel.Todo.t) (st : Document.document) : Document.parsing_end_info =
   if n <= 0 then (Stdlib.Format.eprintf "handle_d_events run out of steps:\nTodo = %a\n" (Sel.Todo.pp Document.pp_event) events; Stdlib.exit 1)
   else if Sel.Todo.is_empty events then assert false
   else begin
diff --git a/language-server/tests/d_tests.ml b/language-server/tests/d_tests.ml
index dad8cc612..e6c563d21 100644
--- a/language-server/tests/d_tests.ml
+++ b/language-server/tests/d_tests.ml
@@ -5,8 +5,8 @@ open Base
 
 [@@@warning "-27"]
 
-let validate_document doc =
-  let doc, events = Document.validate_document doc in
+let validate_document parsed_document =
+  let doc, events = Document.validate_document parsed_document in
   let todo = Sel.Todo.add Sel.Todo.empty events in
   handle_d_events todo doc
 
@@ -20,32 +20,32 @@ let trdeps doc s1 =
 
 
 let%test_unit "parse.validate_errors_twice" = 
-  let _, _, _, doc = init_and_parse_test_doc ~text:"Lemma a : True. Proof. idtac (fun x -> x). Qed." in
-  let unchanged, invalid, _, doc = validate_document doc in
-  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
-  let s1,(s2,(s3,(s4,()))) = d_sentences doc (P(P(E(P(O))))) in
-  [%test_eq: sentence_id option] (Some s4.id) unchanged;
-  let _, _, _, doc = validate_document doc in
-  [%test_eq: int] (List.length (Document.parse_errors doc)) 1;
-  let _, _, _, doc= validate_document doc in
-  [%test_eq: int] (List.length (Document.parse_errors doc)) 1
+  let Document.{parsed_document} = init_and_parse_test_doc ~text:"Lemma a : True. Proof. idtac (fun x -> x). Qed." in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = validate_document parsed_document in
+  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid_ids);
+  let s1,(s2,(s3,(s4,()))) = d_sentences parsed_document (P(P(E(P(O))))) in
+  [%test_eq: sentence_id option] (Some s4.id) unchanged_id;
+  let Document.{parsed_document} = validate_document parsed_document in
+  [%test_eq: int] (List.length (Document.parse_errors parsed_document)) 1;
+  let Document.{parsed_document}= validate_document parsed_document in
+  [%test_eq: int] (List.length (Document.parse_errors parsed_document)) 1
 
 let %test_unit "document: invalidate top" =
-  let _, _, _, doc = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
-  let unchanged, invalid, _, doc = validate_document doc in
-  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
-  let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  [%test_eq: sentence_id option] (Some s5.id) unchanged;
-  let doc = Document.apply_text_edits doc [Document.range_of_id doc s1.id,"Definition x := 4."] in
-  let unchanged, invalid, _, doc = validate_document doc in
-  let r1,(r2,(r3,(r4,(r5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  [%test_eq: sentence_id list] [s1.id] (Stateid.Set.elements invalid);
-  [%test_eq: sentence_id option] None unchanged;
+  let Document.{parsed_document} = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = validate_document parsed_document in
+  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid_ids);
+  let s1,(s2,(s3,(s4,(s5,())))) = d_sentences parsed_document (P(P(P(P(P(O)))))) in
+  [%test_eq: sentence_id option] (Some s5.id) unchanged_id;
+  let parsed_document = Document.apply_text_edits parsed_document [Document.range_of_id parsed_document s1.id,"Definition x := 4."] in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = validate_document parsed_document in
+  let r1,(r2,(r3,(r4,(r5,())))) = d_sentences parsed_document (P(P(P(P(P(O)))))) in
+  [%test_eq: sentence_id list] [s1.id] (Stateid.Set.elements invalid_ids);
+  [%test_eq: sentence_id option] None unchanged_id;
   [%test_eq: sentence_id] s2.id r2.id;
   [%test_eq: sentence_id] s3.id r3.id;
   [%test_eq: sentence_id] s4.id r4.id;
   [%test_eq: sentence_id] s5.id r5.id;
-  let deps = trdeps doc s1 in
+  let deps = trdeps parsed_document s1 in
   [%test_pred: sentence_id] (fun x -> Stateid.Set.mem x deps) r2.id;
   [%test_pred: sentence_id] (fun x -> Stateid.Set.mem x deps) r3.id;
   [%test_pred: sentence_id] (fun x -> Stateid.Set.mem x deps) r4.id;
@@ -53,21 +53,21 @@ let %test_unit "document: invalidate top" =
   ()
 
 let %test_unit "document: invalidate proof" =
-  let _, _, _, doc = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
-  let unchanged, invalid, _, doc = validate_document doc in
-  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
-  let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  [%test_eq: sentence_id option] (Some s5.id) unchanged;
-  let doc = Document.apply_text_edits doc [Document.range_of_id doc s3.id,"idtac."] in
-  let unchanged, invalid, _, doc = validate_document doc in
-  let r1,(r2,(r3,(r4,(r5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  [%test_eq: sentence_id list] [s3.id] (Stateid.Set.elements invalid);
-  [%test_eq: sentence_id option] (Some s2.id) unchanged;
+  let Document.{parsed_document} = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = validate_document parsed_document in
+  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid_ids);
+  let s1,(s2,(s3,(s4,(s5,())))) = d_sentences parsed_document (P(P(P(P(P(O)))))) in
+  [%test_eq: sentence_id option] (Some s5.id) unchanged_id;
+  let parsed_document = Document.apply_text_edits parsed_document [Document.range_of_id parsed_document s3.id,"idtac."] in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = validate_document parsed_document in
+  let r1,(r2,(r3,(r4,(r5,())))) = d_sentences parsed_document (P(P(P(P(P(O)))))) in
+  [%test_eq: sentence_id list] [s3.id] (Stateid.Set.elements invalid_ids);
+  [%test_eq: sentence_id option] (Some s2.id) unchanged_id;
   [%test_eq: sentence_id] s1.id r1.id;
   [%test_eq: sentence_id] s2.id r2.id;
   [%test_eq: sentence_id] s4.id r4.id;
   [%test_eq: sentence_id] s5.id r5.id;
-  let deps = trdeps doc s3 in
+  let deps = trdeps parsed_document s3 in
   [%test_pred: sentence_id] (fun x -> not (Stateid.Set.mem x deps)) r1.id;
   [%test_pred: sentence_id] (fun x -> not (Stateid.Set.mem x deps)) r2.id;
   [%test_pred: sentence_id] (fun x -> not (Stateid.Set.mem x deps)) r3.id;
@@ -76,37 +76,37 @@ let %test_unit "document: invalidate proof" =
 
 
 let %test_unit "document: invalidate proof 2" =
-  let _, _, _, doc = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
-  let unchanged, invalid, _, doc = validate_document doc in
-  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
-  let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  [%test_eq: sentence_id option] (Some s5.id) unchanged;
-  let doc = Document.apply_text_edits doc [Document.range_of_id doc s3.id,""] in
-  let unchanged, invalid, _, doc = validate_document doc in
-  let r1,(r2,(r3,(r4,()))) = d_sentences doc (P(P(P(P(O))))) in
-  [%test_eq: sentence_id list] [s3.id;s4.id;s5.id] (Stateid.Set.elements invalid);
-  [%test_eq: sentence_id option] (Some s2.id) unchanged;
+  let Document.{parsed_document} = init_and_parse_test_doc ~text:"Definition x := 3. Lemma foo : x = 3. Proof. reflexivity. Qed." in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = validate_document parsed_document in
+  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid_ids);
+  let s1,(s2,(s3,(s4,(s5,())))) = d_sentences parsed_document (P(P(P(P(P(O)))))) in
+  [%test_eq: sentence_id option] (Some s5.id) unchanged_id;
+  let parsed_document = Document.apply_text_edits parsed_document [Document.range_of_id parsed_document s3.id,""] in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = validate_document parsed_document in
+  let r1,(r2,(r3,(r4,()))) = d_sentences parsed_document (P(P(P(P(O))))) in
+  [%test_eq: sentence_id list] [s3.id;s4.id;s5.id] (Stateid.Set.elements invalid_ids);
+  [%test_eq: sentence_id option] (Some s2.id) unchanged_id;
   [%test_eq: sentence_id] s1.id r1.id;
   [%test_eq: sentence_id] s2.id r2.id
 
 let %test_unit "document: delete line" = 
-  let unchanged, invalid, _, doc = init_and_parse_test_doc ~text:"Definition x:= 3. Lemma foo : x = 3. Proof. reflexitivity. Qed." in 
-  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
-  let s1,(s2,(s3,(s4,(s5,())))) = d_sentences doc (P(P(P(P(P(O)))))) in
-  let doc = Document.apply_text_edits doc [Document.range_of_id doc s5.id,""] in
-  let unchanged, invalid, _, doc = validate_document doc in 
-  let sentences_id = Stateid.Set.of_list (List.map (Document.sentences doc) ~f:(fun s -> s.id)) in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = init_and_parse_test_doc ~text:"Definition x:= 3. Lemma foo : x = 3. Proof. reflexitivity. Qed." in 
+  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid_ids);
+  let s1,(s2,(s3,(s4,(s5,())))) = d_sentences parsed_document (P(P(P(P(P(O)))))) in
+  let parsed_document = Document.apply_text_edits parsed_document [Document.range_of_id parsed_document s5.id,""] in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = validate_document parsed_document in 
+  let sentences_id = Stateid.Set.of_list (List.map (Document.sentences parsed_document) ~f:(fun s -> s.id)) in
   [%test_pred: sentence_id] (fun x -> not (Stateid.Set.mem x sentences_id)) s5.id;
   ()
 
 let %test_unit "document: expand sentence" =
-  let unchanged, invalid, _, doc = init_and_parse_test_doc ~text:"Lemma foo : x = 3. M." in
-  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid);
-  let s1,(s2,()) = d_sentences doc (P(P(O))) in
-  let range = Document.range_of_id doc s2.id in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = init_and_parse_test_doc ~text:"Lemma foo : x = 3. M." in
+  [%test_eq: sentence_id list] [] (Stateid.Set.elements invalid_ids);
+  let s1,(s2,()) = d_sentences parsed_document (P(P(O))) in
+  let range = Document.range_of_id parsed_document s2.id in
   let new_range = Lsp.Types.Range.{ start = range.end_; end_ = range.end_ } in
-  let doc = Document.apply_text_edits doc [new_range,"foo."] in
-  let unchanged, invalid, _, doc = validate_document doc in
-  let r1,(r2,()) = d_sentences doc (P(P(O))) in
+  let parsed_document = Document.apply_text_edits parsed_document [new_range,"foo."] in
+  let Document.{unchanged_id; invalid_ids; parsed_document} = validate_document parsed_document in
+  let r1,(r2,()) = d_sentences parsed_document (P(P(O))) in
   [%test_eq: sentence_id] s1.id r1.id;
   ()
\ No newline at end of file
diff --git a/language-server/tests/dm_tests.ml b/language-server/tests/dm_tests.ml
index a3fd1a7e5..43c7b4ab8 100644
--- a/language-server/tests/dm_tests.ml
+++ b/language-server/tests/dm_tests.ml
@@ -83,7 +83,7 @@ let%test_unit "parse.extensions" =
 let%test_unit "parse.invalidate_before_module" =
   let st, init_events = em_init_test_doc ~text:"Check nat. Module M := Nat." in
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   check_no_diag st;
@@ -93,7 +93,7 @@ let%test_unit "parse.invalidate_before_module" =
 
 let%test_unit "exec.init" =
   let st, init_events = em_init_test_doc ~text:"Definition x := true. Definition y := false." in
-  let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   let ranges = (DocumentManager.executed_ranges st Settings.Mode.Manual).processed in
@@ -106,7 +106,7 @@ let%test_unit "exec.init" =
 let%test_unit "exec.require_error" =
   let st, init_events = em_init_test_doc ~text:"Require fuhidkgjh. Definition x := true." in
   let st, (s1, (s2, ())) = dm_parse st (E(P O)) in
-  let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   let ranges = (DocumentManager.executed_ranges st Settings.Mode.Manual).processed in
@@ -116,10 +116,10 @@ let%test_unit "exec.require_error" =
 let%test_unit "step_forward.delete_observe_id" =
   let st, init_events = em_init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3." in 
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add todo events) in
   let st = handle_dm_events todo st in
   [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st);
@@ -130,10 +130,10 @@ let%test_unit "step_forward.delete_observe_id" =
 let%test_unit "step_forward.expand_sentence_observe_id" =
   let st, init_events = em_init_test_doc ~text:"Definition x := 3. P." in 
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add todo events) in
   let st = handle_dm_events todo st in
   [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st);
@@ -146,10 +146,10 @@ let%test_unit "step_forward.expand_sentence_observe_id" =
 let%test_unit "step_forward.insert_space_after_sentence_observe_id" =
   let st, init_events = em_init_test_doc ~text:"Definition x := 3. P." in 
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add todo events) in
   let st = handle_dm_events todo st in
   [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st);
@@ -162,13 +162,13 @@ let%test_unit "step_forward.insert_space_after_sentence_observe_id" =
 let%test_unit "step_forward.proof_view" =
   let st, init_events = em_init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3." in 
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add todo events) in
   let st = handle_dm_events todo st in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add todo events) in
   let st = handle_dm_events todo st in
   [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st);
@@ -182,7 +182,7 @@ let%test_unit "step_forward.proof_view" =
 let%test_unit "step_forward.document_begin" =
   let st, init_events = em_init_test_doc ~text:"(* Some comment *)\nLemma foo : x = 3." in
   let st, (s1, ()) = dm_parse st (P O) in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in 
   [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s1.id)) (DocumentManager.Internal.observe_id st)
@@ -190,11 +190,11 @@ let%test_unit "step_forward.document_begin" =
 let%test_unit "step_backward.document_begin" =
   let st, init_events = em_init_test_doc ~text:"(* Some comment *)\nLemma foo : x = 3." in
   let st, (s1, ()) = dm_parse st (P O) in
-  let st, events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   let todo = Sel.Todo.(add init_events events) in
-  let st, events = DocumentManager.interpret_to_previous st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_previous st Settings.Mode.Manual in
   let st = handle_dm_events todo st in
   [%test_eq: bool] (Option.is_none (DocumentManager.Internal.observe_id st)) true
 
@@ -216,7 +216,7 @@ let%test_unit "exec.insert" =
 let%test_unit "edit.shift_warning_in_sentence" =
   let st, init_events = em_init_test_doc ~text:"#[deprecated(note = \"foo\", since = \"foo\")] Definition x := true. Definition y := x." in
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   check_diag st [
@@ -239,7 +239,7 @@ let%test_unit "edit.shift_warning_in_sentence" =
 let%test_unit "edit.shift_warning_before_sentence" =
   let st, init_events = em_init_test_doc ~text:"#[deprecated(note = \"foo\", since = \"foo\")] Definition x := true. Definition y := x." in
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   check_diag st [
@@ -259,7 +259,7 @@ let%test_unit "edit.shift_warning_before_sentence" =
 let%test_unit "edit.shift_error_in_sentence" =
   let st, init_events = em_init_test_doc ~text:"Definition x := true. Definition y := z." in
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   check_diag st [
@@ -282,7 +282,7 @@ let%test_unit "edit.shift_error_in_sentence" =
 let%test_unit "edit.shift_error_before_sentence" =
   let st, init_events = em_init_test_doc ~text:"Definition x := true. Definition y := z." in
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   check_diag st [
@@ -302,7 +302,7 @@ let%test_unit "edit.shift_error_before_sentence" =
 let%test_unit "edit.edit_non_root_observe_id_top" =
   let st, init_events = em_init_test_doc ~text:"Definition x := 1. Definition y := 2." in
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   let st = edit_text st ~start:0 ~stop:18 ~text:"Definition x := 3." in
@@ -312,7 +312,7 @@ let%test_unit "edit.edit_non_root_observe_id_top" =
 let%test_unit "edit.edit_non_root_observe_id" =
   let st, init_events = em_init_test_doc ~text:"Definition x := 1. Definition y := 2. Definition z := 3." in
   let st, (s1, (s2, (s3, ()))) = dm_parse st (P(P(P O))) in
-  let st, events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add init_events events) in
   let st = handle_dm_events todo st in
   let st = edit_text st ~start:19 ~stop:37 ~text:"Definition y := 4." in
diff --git a/language-server/tests/em_tests.ml b/language-server/tests/em_tests.ml
index d66f076c5..745ee0630 100644
--- a/language-server/tests/em_tests.ml
+++ b/language-server/tests/em_tests.ml
@@ -24,7 +24,7 @@ let set_delegation_mode mode =
 let%test_unit "exec: finished proof" =
   let st, events = em_init_test_doc ~text:"Lemma x : True. trivial. Qed. Check x." in
   let st, (s1, (s2, (s3, (s4, ())))) = dm_parse st (P(P(P(P O)))) in
-  let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add events exec_events) in
   let st = handle_dm_events todo st in
   check_diag st [
@@ -35,7 +35,7 @@ let%test_unit "exec: finished proof skip" =
   let st, events = em_init_test_doc ~text:"Lemma x : True. trivial. Qed. Check x." in
   let st, (s1, (s2, (s3, (s4, ())))) = dm_parse st (P(P(P(P O)))) in
   set_delegation_mode SkipProofs;
-  let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add events exec_events) in
   let st = handle_dm_events todo st in
   check_diag st [
@@ -46,7 +46,7 @@ let%test_unit "exec: finished proof skip" =
 let%test_unit "exec: unfinished proof" =
   let st, events = em_init_test_doc ~text:"Lemma x : True. Qed. Check x." in
   let st, (s1, (s2, (s3, ()))) = dm_parse st (P(P(P O))) in
-  let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add events exec_events) in
   let st = handle_dm_events todo st in
   let errors = ExecutionManager.all_errors (DocumentManager.Internal.execution_state st) in
@@ -62,7 +62,7 @@ let%test_unit "exec: unfinished proof skip" =
   let st, events = em_init_test_doc ~text:"Lemma x : True. Qed. Check x." in
   let st, (s1, (s2, (s3, ()))) = dm_parse st (P(P(P O))) in
   set_delegation_mode SkipProofs;
-  let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add events exec_events) in
   let st = handle_dm_events todo st in
   check_diag st [
@@ -77,7 +77,7 @@ let%test_unit "exec: unfinished proof delegate" =
   let st, events = em_init_test_doc ~text:"Lemma x : True. Qed. Check x." in
   let st, (s1, (s2, (s3, ()))) = dm_parse st (P(P(P O))) in
   set_delegation_mode (DelegateProofsToWorkers { number_of_workers = 1 });
-  let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add events exec_events) in
   let st = handle_dm_events todo st in
   check_diag st [
@@ -92,7 +92,7 @@ let%test_unit "exec: unfinished proof delegate" =
 let%test_unit "exec: unstarted proof" =
   let st, events = em_init_test_doc ~text:"Qed. Check nat." in
   let st, (s1, (s2, ())) = dm_parse st (P(P O)) in
-  let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add events exec_events) in
   let st = handle_dm_events todo st in
   check_diag st [
diff --git a/language-server/tests/goals.ml b/language-server/tests/goals.ml
index 25e3cfd79..28f9541cf 100644
--- a/language-server/tests/goals.ml
+++ b/language-server/tests/goals.ml
@@ -20,13 +20,13 @@ open Protocol
 let%test_unit "goals: encoding after replay from top" =
   let st = dm_init_and_parse_test_doc ~text:"Lemma foo : forall x y, x + y = y + x." in
   let st, (_s1, ()) = dm_parse st (P O) in
-  let st, exec_events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add empty exec_events) in
   let st = handle_dm_events todo st in
-  let st, exec_events = DocumentManager.interpret_to_previous st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_previous st Settings.Mode.Manual in
   let todo = Sel.Todo.(add empty exec_events) in
   let st = handle_dm_events todo st in
-  let st, exec_events = DocumentManager.interpret_to_next st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_next st Settings.Mode.Manual in
   let todo = Sel.Todo.(add empty exec_events) in
   let st = handle_dm_events todo st in
   let proof = Stdlib.Option.get (DocumentManager.get_proof st Protocol.Settings.Goals.Diff.Mode.Off None) in
@@ -37,7 +37,7 @@ let%test_unit "goals: encoding after replay from top" =
 let%test_unit "goals: proof is available after error" =
   let st = dm_init_and_parse_test_doc ~text:"Lemma foo : False. easy." in
   let st, (_s1, (_s2, ())) = dm_parse st (P (P O)) in
-  let st, exec_events = DocumentManager.interpret_to_end st ~check_mode:Settings.Mode.Manual in
+  let st, exec_events = DocumentManager.interpret_to_end st Settings.Mode.Manual in
   let todo = Sel.Todo.(add empty exec_events) in
   let st = handle_dm_events todo st in
   let proof = DocumentManager.get_proof st Protocol.Settings.Goals.Diff.Mode.Off None in