fix: make the return type of Document.handle_event into a record

This makes the code way more readable

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 -> 

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

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

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

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

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,54 +20,54 @@ 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;
   [%test_pred: sentence_id] (fun x -> Stateid.Set.mem x deps) r5.id;
   ()
 
 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;
   ()