cleanup: remove unecessary interpret_in_background API

The move to a unified model with an observe id in both
continuous and manual modes has made the need for a
seperate execution API redundant.

language-server/dm/documentManager.ml

@@ -268,8 +268,8 @@ let get_info_messages st pos =
     let feedback = feedback |> List.filter info in
     List.map (fun (lvl,_oloc,_,msg) -> DiagnosticSeverity.of_feedback_level lvl, pp_of_coqpp msg) feedback
 
-let create_execution_event background event =
-  let priority = if background then None else Some PriorityManager.execution in
+let create_execution_event event =
+  let priority = Some PriorityManager.execution in
   Sel.now ?priority event
 
 let state_before_error state error_id =
@@ -288,15 +288,15 @@ let state_before_error state error_id =
       let observe_id = (Id id) in
       {state with observe_id}, Some last_range
 
-let observe ~background state id ~should_block_on_error : (state * event Sel.Event.t list) =
+let observe state id ~should_block_on_error : (state * event Sel.Event.t list) =
   match Document.get_sentence state.document id with
   | None -> state, [] (* TODO error? *)
   | Some { id } ->
     Option.iter Sel.Event.cancel state.cancel_handle;
     let vst_for_next_todo, execution_state, task, error_id = ExecutionManager.build_tasks_for state.document (Document.schedule state.document) state.execution_state id should_block_on_error in
     match task with
     | Some task -> (* task will only be Some if there is no error *)
-        let event = create_execution_event background (Execute {id; vst_for_next_todo; task; started = Unix.gettimeofday ()}) in
+        let event = create_execution_event (Execute {id; vst_for_next_todo; task; started = Unix.gettimeofday ()}) in
         let cancel_handle = Some (Sel.Event.get_cancellation_handle event) in
         {state with execution_state; cancel_handle}, [event]
     | None ->
@@ -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,22 +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
-
-let interpret_in_background st ~should_block_on_error =
-  match Document.get_last_sentence st.document with
-  | None -> (st, [])
-  | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); observe ~background:true st id ~should_block_on_error
+    interpret_to st id check_mode
 
 let is_above st id1 id2 =
   let range1 = Document.range_of_id st id1 in
@@ -511,7 +506,7 @@ let execution_finished st id started =
   let state = Some st in
   {state; events=[]; update_view; notification=None}
 
-let execute st id vst_for_next_todo started task background block =
+let execute st id vst_for_next_todo started task block =
   let time = Unix.gettimeofday () -. started in
   match Document.get_sentence st.document id with
   | None ->
@@ -528,7 +523,7 @@ let execute st id vst_for_next_todo started task background block =
         let events = if block then mk_block_on_error_event last_range error_id else [] in
         st, events
       in
-    let event = Option.map (fun task -> create_execution_event background (Execute {id; vst_for_next_todo; task; started })) next in
+    let event = Option.map (fun task -> create_execution_event (Execute {id; vst_for_next_todo; task; started })) next in
     match event, block_events with
       | None, [] -> execution_finished { st with execution_state } id started (* There is no new tasks, and no errors -> execution finished *)
       | _ ->
@@ -565,15 +560,15 @@ 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 =
   match ev with
   | Execute { id; vst_for_next_todo; started; task } ->
-    execute st id vst_for_next_todo started task background block
+    execute st id vst_for_next_todo started task block
   | ExecutionManagerEvent ev ->
     handle_execution_manager_event st ev
   | Observe id ->
     let update_view = true in
-    let st, events = observe st id ~should_block_on_error:block ~background in
+    let st, events = observe st id ~should_block_on_error:block in
     {state=Some st; events; update_view; notification=None}
   | ParseEvent ->
     let document, events = Document.validate_document st.document in
@@ -592,8 +587,8 @@ let handle_event ev st ~block ~background diff_mode =
     | Some (unchanged_id, invalid_roots, prev_document, new_document) ->
       let st = validate_document st unchanged_id invalid_roots prev_document new_document in
       let update_view = true in
-      if background then
-        let (st, events) = interpret_in_background st ~should_block_on_error:block in
+      if check_mode = Settings.Mode.Continuous then
+        let (st, events) = interpret_to_end st check_mode in
         {state=(Some st); events; update_view; notification=None}
       else
         {state=(Some st); events=[]; update_view; notification=None}

language-server/dm/documentManager.mli

@@ -65,30 +65,26 @@ 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 -> 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. *)
 
-val interpret_in_background : state -> should_block_on_error:bool -> (state * events)
-(** [interpret_in_background doc] same as [interpret_to_end] but computation 
-    is done in background (with lower priority) *)
-
 val reset : state -> state * events 
 (** resets Coq *)
 
@@ -116,7 +112,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

@@ -235,7 +235,7 @@ let replace_state path st visible = Hashtbl.replace states path { st; visible}
 let run_documents () =
   let interpret_doc_in_bg path { st : Dm.DocumentManager.state ; visible } events =
       let st = Dm.DocumentManager.reset_to_top st in
-      let (st, events') = Dm.DocumentManager.interpret_in_background st ~should_block_on_error:!block_on_first_error in
+      let (st, events') = Dm.DocumentManager.interpret_to_end st !check_mode in
       let uri = DocumentUri.of_path path in
       replace_state path st visible;
       update_view uri st;
@@ -311,7 +311,7 @@ let textDocumentDidOpen params =
   | Some { st } ->
     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
+        let (st, events) = Dm.DocumentManager.interpret_to_end st !check_mode in
         (st, events)
       else 
         (st, [])
@@ -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
     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 -> ()