feat: new handle event return type for document manager

We will now put the proof view handling in the document manager.
Since ther return type for the handle event function is becoming
quite big, we turn it into a record.

language-server/dm/documentManager.ml

@@ -15,6 +15,7 @@
 open Lsp.Types
 open Protocol
 open Protocol.LspWrapper
+open Protocol.ExtProtocol
 open Protocol.Printing
 open Types
 
@@ -54,6 +55,15 @@ type event =
   | ParseEvent
   | Observe of Types.sentence_id
   | ParseMore of Document.event
+  | SendProofView of Position.t option
+
+type handled_event = {
+    state : state option;
+    events: event Sel.Event.t list;
+    blocking_error: blocking_error option;
+    update_view: bool;
+    notification: Notification.Server.t option;
+}
 
 let pp_event fmt = function
   | Execute { id; started; _ } ->
@@ -65,7 +75,9 @@ let pp_event fmt = function
   | Observe id ->
     Stdlib.Format.fprintf fmt "Observe %d" (Stateid.to_int id)
   | ParseMore _ -> Stdlib.Format.fprintf fmt "ParseMore event"
-
+  | SendProofView pos ->
+    let string_loc = Option.cata Position.to_string "(no position)" pos in
+    Stdlib.Format.fprintf fmt "SendProofView at position %s" @@ string_loc
 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
@@ -469,28 +481,46 @@ let execution_finished st id started =
   log (Printf.sprintf "ExecuteToLoc %d ends after %2.3f" (Stateid.to_int id) time);
   (* We update the state to trigger a publication of diagnostics *)
   let update_view = true in
-  (Some st, [], None, update_view)
+  let state = Some st in
+  {state; events=[]; blocking_error=None; update_view; notification=None}
 
 let execute st id vst_for_next_todo started task background block =
   match Document.get_sentence st.document id with
-  | None -> Some st, [], None, true (* Sentences have been invalidate, probably because the user edited while executing *)
+  | None -> 
+    {state=Some st; events=[]; blocking_error=None; update_view=true; notification=None} (* Sentences have been invalidate, probably because the user edited while executing *)
   | Some _ ->
     let (next, execution_state,vst_for_next_todo,events, exec_error) =
       ExecutionManager.execute st.execution_state st.document (vst_for_next_todo, [], false) task block in
-    let st, error_range =
+    let st, blocking_error =
       match exec_error with
       | None -> st, None
       | Some id -> create_blocking_error_range st id 
       in
     let event = Option.map (fun task -> create_execution_event background (Execute {id; vst_for_next_todo; task; started })) next in
-    match event, error_range with
-    | None, None -> execution_finished { st with execution_state } id started
-    | _ ->
-      let cancel_handle = Option.map Sel.Event.get_cancellation_handle event in
-      let event = Option.cata (fun event -> [event]) [] event in
-      let st = {st with execution_state; cancel_handle} in
-      let update_view = true in
-      (Some st, inject_em_events events @ event, error_range, update_view)
+    match event, blocking_error with
+      | None, None -> execution_finished { st with execution_state } id started
+      | _ ->
+        let cancel_handle = Option.map Sel.Event.get_cancellation_handle event in
+        let event = Option.cata (fun event -> [event]) [] event in
+        let state = Some {st with execution_state; cancel_handle} in
+        let update_view = true in
+        let events = inject_em_events events @ event in
+        {state; events; blocking_error; update_view; notification=None}
+
+let get_proof st diff_mode pos =
+  let previous_st id =
+    let oid = fst @@ Scheduler.task_for_sentence (Document.schedule st.document) id in
+    Option.bind oid (ExecutionManager.get_vernac_state st.execution_state)
+  in
+  let observe_id = 
+    match st.observe_id with
+    | None -> None
+    | Some observe_id -> to_sentence_id observe_id 
+  in
+  let oid = Option.cata (id_of_pos st) observe_id pos in
+  let ost = Option.bind oid (ExecutionManager.get_vernac_state st.execution_state) in
+  let previous = Option.bind oid previous_st in
+  Option.bind ost (ProofState.get_proof ~previous diff_mode)
 
 let handle_execution_manager_event st ev =
   let id, execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in
@@ -505,9 +535,9 @@ let handle_execution_manager_event st ev =
     | _, _ -> Option.map (fun execution_state -> {st with execution_state}) execution_state_update
   in
   let update_view = true in
-  (st, inject_em_events events, None, update_view)
+  {state=st; events=(inject_em_events events);blocking_error=None; update_view; notification=None}
 
-let handle_event ev st block background =
+let handle_event ev st block background diff_mode =
   match ev with
   | Execute { id; vst_for_next_todo; started; task } ->
     execute st id vst_for_next_todo started task background block
@@ -516,41 +546,37 @@ let handle_event ev st block background =
   | Observe id ->
     let update_view = true in
     let st, events, blocking_error = observe st id ~should_block_on_error:block ~background in
-    Some st, events, blocking_error, update_view
+    {state=Some st; events; blocking_error; update_view; notification=None}
   | ParseEvent ->
     let document, events = Document.validate_document st.document in
     let update_view = true in
-    Some {st with document}, inject_doc_events events, None, update_view
+    let state = Some {st with document} in
+    let events = inject_doc_events events in
+    {state; events; blocking_error=None; update_view; notification=None}
   | ParseMore ev ->
     let document, events, update = Document.handle_event st.document ev in
-    match update with
+    begin match update with
     | None ->
       let update_view = false in
-      Some {st with document}, inject_doc_events events, None, update_view
+      let state = Some {st with document} in
+      let events = inject_doc_events events in
+      {state; events; blocking_error=None; update_view; notification=None}
     | Some (unchanged_id, invalid_roots, document) ->
       let st = validate_document st unchanged_id invalid_roots document in
       let update_view = true in
       if background then
         let (st, events, blocking_error) = interpret_in_background st ~should_block_on_error:block in
-        (Some st), events, blocking_error, update_view
+        {state=(Some st); events; blocking_error; update_view; notification=None}
       else
-        (Some st), [], None, update_view
-
-
-let get_proof st diff_mode pos =
-  let previous_st id =
-    let oid = fst @@ Scheduler.task_for_sentence (Document.schedule st.document) id in
-    Option.bind oid (ExecutionManager.get_vernac_state st.execution_state)
-  in
-  let observe_id = 
-    match st.observe_id with
-    | None -> None
-    | Some observe_id -> to_sentence_id observe_id 
-  in
-  let oid = Option.cata (id_of_pos st) observe_id pos in
-  let ost = Option.bind oid (ExecutionManager.get_vernac_state st.execution_state) in
-  let previous = Option.bind oid previous_st in
-  Option.bind ost (ProofState.get_proof ~previous diff_mode)
+        {state=(Some st); events=[]; blocking_error=None; update_view; notification=None}
+    end
+  | SendProofView pos ->
+    let proof = get_proof st diff_mode pos in
+    let messages = get_messages st pos in
+    let params = Notification.Server.ProofViewParams.{ proof; messages} in
+    let notification = Some (Notification.Server.ProofView params) in
+    let update_view = true in
+    {state=(Some st); events=[]; update_view; blocking_error=None; notification}
 
 let context_of_id st = function
   | None -> Some (ExecutionManager.get_initial_context st.execution_state)

language-server/dm/documentManager.mli

@@ -16,6 +16,7 @@ open Types
 open Lsp.Types
 open Protocol
 open Protocol.LspWrapper
+open Protocol.ExtProtocol
 open Protocol.Printing
 open CompletionItems
 
@@ -38,6 +39,14 @@ val pp_event : Format.formatter -> event -> unit
 
 type events = event Sel.Event.t list
 
+type handled_event = {
+    state : state option;
+    events: events;
+    blocking_error: blocking_error option;
+    update_view: bool;
+    notification: Notification.Server.t option;
+}
+
 val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> observe_id option -> state * events
 (** [init st opts uri text] initializes the document manager with initial vernac state
     [st] on which command line opts will be set. [background] indicates if the document should
@@ -112,7 +121,7 @@ val get_proof : state -> Settings.Goals.Diff.Mode.t -> Position.t option -> Proo
 
 val get_completions : state -> Position.t -> (completion_item list, string) Result.t
 
-val handle_event : event -> state -> bool -> bool -> (state option * events * blocking_error option * bool)
+val handle_event : event -> state -> bool -> bool -> 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

@@ -667,14 +667,15 @@ let handle_event = function
       []
     | Some { st; visible } ->
       let background = !check_mode = Settings.Mode.Continuous in
-      let (ost, events, error_range, should_update_view) = Dm.DocumentManager.handle_event e st !block_on_first_error background in
-      begin match ost with
+      let handled_event = Dm.DocumentManager.handle_event e st !block_on_first_error background !diff_mode in
+      let events = handled_event.events in
+      begin match handled_event.state with
         | None -> ()
         | Some st ->
           replace_state (DocumentUri.to_path uri) st visible;
-          if should_update_view then update_view uri st
+          if handled_event.update_view then update_view uri st
       end;
-      match error_range with
+      match handled_event.blocking_error with
       | None ->
         inject_dm_events (uri, events)
       | Some {last_range; error_range} ->