Merge pull request #513 from ejgallego/abstract_callbacks

[fleche] Abstract IO callbacks from LSP transport detail.

controller/coq_lsp.ml

@@ -31,10 +31,10 @@ let exit_message () =
 
 let lsp_cleanup () = exit_message ()
 
-let rec process_queue ~delay ~ofn ~state : unit =
+let rec process_queue ~delay ~io ~ofn ~state : unit =
   if Fleche.Debug.sched_wakeup then
     LIO.trace "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
-  match dispatch_or_resume_check ~ofn ~state with
+  match dispatch_or_resume_check ~io ~ofn ~state with
   | None ->
     (* As of now, we exit the whole program here, we could try an experiment to
        invert the threads, so the I/O routine is a thread and process_queue is
@@ -45,28 +45,30 @@ let rec process_queue ~delay ~ofn ~state : unit =
     exit 0
   | Some (Yield state) ->
     Thread.delay delay;
-    process_queue ~delay ~ofn ~state
-  | Some (Cont state) -> process_queue ~delay ~ofn ~state
+    process_queue ~delay ~io ~ofn ~state
+  | Some (Cont state) -> process_queue ~delay ~io ~ofn ~state
 
-let concise_cb =
+let concise_cb ofn =
   Fleche.Io.CallBack.
     { trace = (fun _hdr ?extra:_ _msg -> ())
+    ; message = (fun ~lvl:_ ~message:_ -> ())
     ; send_diagnostics =
-        (fun ~ofn ~uri ~version diags ->
+        (fun ~uri ~version diags ->
           if List.length diags > 0 then
             Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
-    ; send_fileProgress = (fun ~ofn:_ ~uri:_ ~version:_ _progress -> ())
+    ; send_fileProgress = (fun ~uri:_ ~version:_ _progress -> ())
     }
 
 (* Main loop *)
-let lsp_cb =
+let lsp_cb ofn =
   Fleche.Io.CallBack.
     { trace = LIO.trace
+    ; message = LIO.logMessage
     ; send_diagnostics =
-        (fun ~ofn ~uri ~version diags ->
+        (fun ~uri ~version diags ->
           Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
     ; send_fileProgress =
-        (fun ~ofn ~uri ~version progress ->
+        (fun ~uri ~version progress ->
           Lsp.JFleche.mk_progress ~uri ~version progress |> ofn)
     }
 
@@ -97,7 +99,9 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
   (* Set log channels *)
   let ofn = LIO.send_json Format.std_formatter in
   LIO.set_log_fn ofn;
-  Fleche.Io.CallBack.set lsp_cb;
+
+  let io = lsp_cb ofn in
+  Fleche.Io.CallBack.set io;
 
   (* IMPORTANT: LSP spec forbids any message from server to client before
      initialize is received *)
@@ -130,17 +134,22 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
   try
     (* LSP Server server initialization *)
     let workspaces = lsp_init_loop ~ifn ~ofn ~cmdline ~debug in
-    if !Fleche.Config.v.verbosity < 2 then (
-      LIO.set_log_fn (fun _obj -> ());
-      Fleche.Io.CallBack.set concise_cb);
+    let io =
+      if !Fleche.Config.v.verbosity < 2 then (
+        LIO.set_log_fn (fun _obj -> ());
+        let io = concise_cb ofn in
+        Fleche.Io.CallBack.set io;
+        io)
+      else io
+    in
 
     (* Core LSP loop context *)
     let state = { State.root_state; cmdline; workspaces } in
 
     (* Read workspace state (noop for now) *)
     Cache.read_from_disk ();
 
-    let pfn () : unit = process_queue ~delay ~ofn ~state in
+    let pfn () : unit = process_queue ~delay ~io ~ofn ~state in
     let (_ : Thread.t) = Thread.create pfn () in
 
     read_loop ()

controller/lsp_core.ml

@@ -168,7 +168,7 @@ end = struct
     let f pr =
       let () =
         let request = Request.Data.dm_request pr in
-        Doc_manager.Request.remove { id; request }
+        Fleche.Theory.Request.remove { id; request }
       in
       Error (code, message)
     in
@@ -188,7 +188,7 @@ end = struct
 
   let query ~ofn ~id (pr : Request.Data.t) =
     let request = Request.Data.dm_request pr in
-    match Doc_manager.Request.add { id; request } with
+    match Fleche.Theory.Request.add { id; request } with
     | Cancel ->
       let code = -32802 in
       let message = "Document is not ready" in
@@ -218,16 +218,16 @@ end
 (***********************************************************************)
 (* Start of protocol handlers: document notifications                  *)
 
-let do_open ~ofn ~(state : State.t) params =
+let do_open ~io ~(state : State.t) params =
   let document =
     field "textDocument" params
     |> Lsp.Doc.TextDocumentItem.of_yojson |> Result.get_ok
   in
   let Lsp.Doc.TextDocumentItem.{ uri; version; text; _ } = document in
   let root_state, workspace = State.workspace_of_uri ~uri ~state in
-  Doc_manager.create ~ofn ~root_state ~workspace ~uri ~raw:text ~version
+  Fleche.Theory.create ~io ~root_state ~workspace ~uri ~raw:text ~version
 
-let do_change ~ofn params =
+let do_change ~ofn ~io params =
   let uri, version = Helpers.get_uri_version params in
   let changes = List.map U.to_assoc @@ list_field "contentChanges" params in
   match changes with
@@ -240,14 +240,14 @@ let do_change ~ofn params =
     ()
   | change :: _ ->
     let raw = string_field "text" change in
-    let invalid_rq = Doc_manager.change ~ofn ~uri ~version ~raw in
+    let invalid_rq = Fleche.Theory.change ~io ~uri ~version ~raw in
     let code = -32802 in
     let message = "Request got old in server" in
     Int.Set.iter (Rq.cancel ~ofn ~code ~message) invalid_rq
 
 let do_close ~ofn:_ params =
   let uri = Helpers.get_uri params in
-  Doc_manager.close ~uri
+  Fleche.Theory.close ~uri
 
 let do_trace params =
   let trace = string_field "value" params in
@@ -369,15 +369,15 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
     Loop
 
 (** Dispatching *)
-let dispatch_notification ~ofn ~state ~method_ ~params : unit =
+let dispatch_notification ~io ~ofn ~state ~method_ ~params : unit =
   match method_ with
   (* Lifecycle *)
   | "exit" -> raise Lsp_exit
   (* setTrace *)
   | "$/setTrace" -> do_trace params
   (* Document lifetime *)
-  | "textDocument/didOpen" -> do_open ~ofn ~state params
-  | "textDocument/didChange" -> do_change ~ofn params
+  | "textDocument/didOpen" -> do_open ~io ~state params
+  | "textDocument/didChange" -> do_change ~io ~ofn params
   | "textDocument/didClose" -> do_close ~ofn params
   | "textDocument/didSave" -> Cache.save_to_disk ()
   (* Cancel Request *)
@@ -387,13 +387,13 @@ let dispatch_notification ~ofn ~state ~method_ ~params : unit =
   (* Generic handler *)
   | msg -> LIO.trace "no_handler" msg
 
-let dispatch_state_notification ~ofn ~state ~method_ ~params : State.t =
+let dispatch_state_notification ~io ~ofn ~state ~method_ ~params : State.t =
   match method_ with
   (* Workspace *)
   | "workspace/didChangeWorkspaceFolders" ->
     do_changeWorkspaceFolders ~ofn ~state params
   | _ ->
-    dispatch_notification ~ofn ~state ~method_ ~params;
+    dispatch_notification ~io ~ofn ~state ~method_ ~params;
     state
 
 let dispatch_request ~method_ ~params : Rq.Action.t =
@@ -424,18 +424,18 @@ let dispatch_request ~method_ ~params : Rq.Action.t =
 let dispatch_request ~ofn ~id ~method_ ~params =
   dispatch_request ~method_ ~params |> Rq.serve ~ofn ~id
 
-let dispatch_message ~ofn ~state (com : LSP.Message.t) : State.t =
+let dispatch_message ~io ~ofn ~state (com : LSP.Message.t) : State.t =
   match com with
   | Notification { method_; params } ->
-    dispatch_state_notification ~ofn ~state ~method_ ~params
+    dispatch_state_notification ~io ~ofn ~state ~method_ ~params
   | Request { id; method_; params } ->
     dispatch_request ~ofn ~id ~method_ ~params;
     state
 
 (* Queue handling *)
 
 (***********************************************************************)
-(* The queue strategy is: we keep pending document checks in Doc_manager, they
+(* The queue strategy is: we keep pending document checks in Fleche.Theory, they
    are only resumed when the rest of requests in the queue are served.
 
    Note that we should add a method to detect stale requests; maybe cancel them
@@ -445,34 +445,34 @@ type 'a cont =
   | Cont of 'a
   | Yield of 'a
 
-let check_or_yield ~ofn ~state =
-  match Doc_manager.Check.maybe_check ~ofn with
+let check_or_yield ~io ~ofn ~state =
+  match Fleche.Theory.Check.maybe_check ~io with
   | None -> Yield state
   | Some (ready, doc) ->
     let () = Rq.serve_postponed ~ofn ~doc ready in
     Cont state
 
 let request_queue = Queue.create ()
 
-let dispatch_or_resume_check ~ofn ~state =
+let dispatch_or_resume_check ~io ~ofn ~state =
   match Queue.peek_opt request_queue with
   | None ->
     (* This is where we make progress on document checking; kind of IDLE
        workqueue. *)
     Control.interrupt := false;
-    check_or_yield ~ofn ~state
+    check_or_yield ~io ~ofn ~state
   | Some com ->
     (* TODO: optimize the queue? EJGA: I've found that VS Code as a client keeps
        the queue tidy by itself, so this works fine as now *)
     ignore (Queue.pop request_queue);
     LIO.trace "process_queue" ("Serving Request: " ^ LSP.Message.method_ com);
     (* We let Coq work normally now *)
     Control.interrupt := false;
-    Cont (dispatch_message ~ofn ~state com)
+    Cont (dispatch_message ~io ~ofn ~state com)
 
 (* Wrapper for the top-level call *)
-let dispatch_or_resume_check ~ofn ~state =
-  try Some (dispatch_or_resume_check ~ofn ~state) with
+let dispatch_or_resume_check ~io ~ofn ~state =
+  try Some (dispatch_or_resume_check ~io ~ofn ~state) with
   | U.Type_error (msg, obj) ->
     LIO.trace_object msg obj;
     Some (Yield state)

controller/lsp_core.mli

@@ -52,7 +52,10 @@ type 'a cont =
 (** Core scheduler: dispatch an LSP request or notification, check document and
     wake up pending requests *)
 val dispatch_or_resume_check :
-  ofn:(Yojson.Safe.t -> unit) -> state:State.t -> State.t cont option
+     io:Fleche.Io.CallBack.t
+  -> ofn:(Yojson.Safe.t -> unit)
+  -> state:State.t
+  -> State.t cont option
 
 (** Add a message to the queue *)
 val enqueue_message : Lsp.Base.Message.t -> unit

controller/request.ml

@@ -48,9 +48,9 @@ module Data = struct
 
   let dm_request pr =
     match pr with
-    | DocRequest { uri; handler = _ } -> Doc_manager.Request.(FullDoc { uri })
+    | DocRequest { uri; handler = _ } -> Fleche.Theory.Request.(FullDoc { uri })
     | PosRequest { uri; point; version; postpone; handler = _ } ->
-      Doc_manager.Request.(PosInDoc { uri; point; version; postpone })
+      Fleche.Theory.Request.(PosInDoc { uri; point; version; postpone })
 
   let serve ~doc pr =
     match pr with

controller/request.mli

@@ -39,6 +39,6 @@ module Data : sig
 
   (* Debug printing *)
   val data : Format.formatter -> t -> unit
-  val dm_request : t -> Doc_manager.Request.request
+  val dm_request : t -> Fleche.Theory.Request.request
   val serve : doc:Fleche.Doc.t -> t -> R.t
 end

editor/code/lib/types.ts

@@ -117,6 +117,7 @@ export interface SentencePerfParams {
 }
 
 export interface DocumentPerfParams {
+  textDocument: VersionedTextDocumentIdentifier;
   summary: string;
   timings: SentencePerfParams[];
 }