cleanup: make document manager api cleaner

language-server/dm/documentManager.ml

@@ -323,7 +323,7 @@ let get_document_symbols st =
   in
   List.map to_document_symbol outline
 
-let interpret_to st id ~check_mode =
+let interpret_to st id check_mode =
   let observe_id = (Id id) in
   let st = { st with observe_id} in
   match check_mode with
@@ -336,22 +336,22 @@ let interpret_to st id ~check_mode =
     | true -> st, [mk_proof_view_event id]
     | false -> st, []
 
-let interpret_to_next_position st pos ~check_mode =
+let interpret_to_next_position st pos check_mode =
   match id_of_sentence_after_pos st pos with
   | None -> (st, []) (* document is empty *)
   | Some id ->
-    let st, events = interpret_to st id ~check_mode in
+    let st, events = interpret_to st id check_mode in
     (st, events)
 
-let interpret_to_position st pos ~check_mode ~point_interp_mode =
+let interpret_to_position st pos check_mode ~point_interp_mode =
   match point_interp_mode with
   | Settings.PointInterpretationMode.Cursor ->
     begin match id_of_pos st pos with
     | None -> (st, []) (* document is empty *)
-    | Some id -> interpret_to st id ~check_mode
+    | Some id -> interpret_to st id check_mode
     end
   | Settings.PointInterpretationMode.NextCommand ->
-    interpret_to_next_position st pos ~check_mode
+    interpret_to_next_position st pos check_mode
 
 let get_next_range st pos =
   match id_of_pos st pos with
@@ -375,7 +375,7 @@ let get_previous_range st pos =
       | None -> Some (Document.range_of_id st.document id)
       | Some { id } -> Some (Document.range_of_id st.document id)
 
-let interpret_to_previous st ~check_mode =
+let interpret_to_previous st check_mode =
   match st.observe_id with
   | Top -> (st, [])
   | (Id id) ->
@@ -388,18 +388,18 @@ let interpret_to_previous st ~check_mode =
         let range = Range.top () in
         { st with observe_id=Top }, [mk_move_cursor_event range]
       | Some { id } -> 
-        let st, events = interpret_to st id ~check_mode in
+        let st, events = interpret_to st id check_mode in
         let range = Document.range_of_id st.document id in
         let mv_cursor = mk_move_cursor_event range in
         st, [mv_cursor] @ events
 
-let interpret_to_next st ~check_mode =
+let interpret_to_next st check_mode =
   match st.observe_id with
   | Top ->
     begin match Document.get_first_sentence st.document with
     | None -> st, [] (*The document is empty*)
     | Some { id } -> 
-      let st, events = interpret_to st id ~check_mode in
+      let st, events = interpret_to st id check_mode in
       let range = Document.range_of_id st.document id in
       let mv_cursor = mk_move_cursor_event range in
       st, [mv_cursor] @ events
@@ -411,17 +411,17 @@ let interpret_to_next st ~check_mode =
       match Document.find_sentence_after st.document (stop+1) with
       | None -> st, []
       | Some { id } -> 
-        let st, events = interpret_to st id ~check_mode in
+        let st, events = interpret_to st id check_mode in
         let range = Document.range_of_id st.document id in
         let mv_cursor = mk_move_cursor_event range in
         st, [mv_cursor] @ events
 
-let interpret_to_end st ~check_mode =
+let interpret_to_end st check_mode =
   match Document.get_last_sentence st.document with
   | None -> (st, [])
   | Some {id} -> 
     log ("interpret_to_end id = " ^ Stateid.to_string id);
-    interpret_to st id ~check_mode
+    interpret_to st id check_mode
 
 let interpret_in_background st ~should_block_on_error =
   match Document.get_last_sentence st.document with
@@ -565,7 +565,8 @@ let handle_execution_manager_event st ev =
   let update_view = true in
   {state=st; events=(inject_em_events events); update_view; notification=None}
 
-let handle_event ev st ~block ~background diff_mode =
+let handle_event ev st ~block check_mode diff_mode =
+  let background = check_mode = Settings.Mode.Continuous in
   match ev with
   | Execute { id; vst_for_next_todo; started; task } ->
     execute st id vst_for_next_todo started task background block

language-server/dm/documentManager.mli

@@ -65,23 +65,23 @@ val get_next_range : state -> Position.t -> Range.t option
 val get_previous_range : state -> Position.t -> Range.t option
 (** [get_previous_pos st pos] get the range of the previous sentence relative to pos *)
 
-val interpret_to_position : state -> Position.t -> check_mode:Settings.Mode.t -> point_interp_mode:Settings.PointInterpretationMode.t -> (state * events)
+val interpret_to_position : state -> Position.t -> Settings.Mode.t -> point_interp_mode:Settings.PointInterpretationMode.t -> (state * events)
 (** [interpret_to_position state pos check_mode point_interp_mode] navigates to the 
     last sentence ending before or at [pos] and returns the resulting state, events that need to take place, and a possible blocking error. *)
 
-val interpret_to_next_position : state -> Position.t -> check_mode:Settings.Mode.t -> (state * events)
+val interpret_to_next_position : state -> Position.t -> Settings.Mode.t -> (state * events)
 (** [interpret_to_next_position state pos check_mode] navigates
     to the first sentence after or at [pos] (excluding whitespace) and returns the resulting state, events that need to take place, a possible blocking error. *)
 
-val interpret_to_previous : state -> check_mode:Settings.Mode.t -> (state * events)
+val interpret_to_previous : state -> Settings.Mode.t -> (state * events)
 (** [interpret_to_previous doc check_mode] navigates to the previous sentence in [doc]
     and returns the resulting state. *)
 
-val interpret_to_next : state -> check_mode:Settings.Mode.t -> (state * events)
+val interpret_to_next : state -> Settings.Mode.t -> (state * events)
 (** [interpret_to_next doc] navigates to the next sentence in [doc]
     and returns the resulting state. *)
 
-val interpret_to_end : state -> check_mode:Settings.Mode.t -> (state * events)
+val interpret_to_end : state -> Settings.Mode.t -> (state * events)
 (** [interpret_to_end doc] navigates to the last sentence in [doc]
     and returns the resulting state. *)
 
@@ -116,7 +116,7 @@ val get_proof : state -> Settings.Goals.Diff.Mode.t -> sentence_id option -> Pro
 
 val get_completions : state -> Position.t -> (completion_item list, string) Result.t
 
-val handle_event : event -> state -> block:bool -> background:bool -> Settings.Goals.Diff.Mode.t -> handled_event
+val handle_event : event -> state -> block:bool -> Settings.Mode.t -> Settings.Goals.Diff.Mode.t -> handled_event
 (** handles events and returns a new state if it was updated. On top of the next events, it also returns info
     on whether execution has halted due to an error and returns a boolean flag stating whether the view
     should be updated *)

language-server/vscoqtop/lspManager.ml

@@ -393,7 +393,7 @@ 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) = Dm.DocumentManager.interpret_to_position st position ~check_mode:!check_mode ~point_interp_mode:!point_interp_mode
+    let (st, events) = Dm.DocumentManager.interpret_to_position st position !check_mode ~point_interp_mode:!point_interp_mode
     in
     replace_state (DocumentUri.to_path uri) st visible;
     update_view uri st;
@@ -405,7 +405,7 @@ let coqtopStepBackward params =
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log "[stepBackward] ignoring event on non existent document"; []
   | Some { st; visible } ->
-      let (st, events) = Dm.DocumentManager.interpret_to_previous st ~check_mode:!check_mode in
+      let (st, events) = Dm.DocumentManager.interpret_to_previous st !check_mode in
       replace_state (DocumentUri.to_path uri) st visible;
       inject_dm_events (uri,events)
 
@@ -414,7 +414,7 @@ let coqtopStepForward params =
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log "[stepForward] ignoring event on non existent document"; []
   | Some { st; visible } ->
-      let (st, events) = Dm.DocumentManager.interpret_to_next st ~check_mode:!check_mode in
+      let (st, events) = Dm.DocumentManager.interpret_to_next st !check_mode in
       replace_state (DocumentUri.to_path uri) st visible;
       update_view uri st;
       inject_dm_events (uri,events) 
@@ -473,7 +473,7 @@ 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) = Dm.DocumentManager.interpret_to_end st ~check_mode:!check_mode in
+    let (st, events) = Dm.DocumentManager.interpret_to_end st !check_mode in
     replace_state (DocumentUri.to_path uri) st visible;
     update_view uri st;
     inject_dm_events (uri,events)
@@ -639,8 +639,7 @@ let handle_event = function
       log @@ "ignoring event on non-existing document";
       []
     | Some { st; visible } ->
-      let background = !check_mode = Settings.Mode.Continuous in
-      let handled_event = Dm.DocumentManager.handle_event e st ~block:!block_on_first_error ~background !diff_mode in
+      let handled_event = Dm.DocumentManager.handle_event e st ~block:!block_on_first_error !check_mode !diff_mode in
       let events = handled_event.events in
       begin match handled_event.state with
         | None -> ()