Merge pull request #450 from ejgallego/init_async

[lsp] Generalize LSP init loop to support async IO.
ejgallego · Mar 6, 2023 · b6de2dc · b6de2dc
2 parents e0163b3 + c80d8e9
commit b6de2dc
Show file tree

Hide file tree

Showing 3 changed files with 36 additions and 15 deletions.
diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
@@ -86,6 +86,15 @@ let coq_init ~fb_queue ~debug =
 let exit_notification =
   Lsp.Base.Message.(Notification { method_ = "exit"; params = [] })
 
+let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug =
+  match ifn () with
+  | None -> raise Lsp_exit
+  | Some msg -> (
+    match lsp_init_process ~ofn ~cmdline ~debug msg with
+    | Init_effect.Exit -> raise Lsp_exit
+    | Init_effect.Loop -> lsp_init_loop ~ifn ~ofn ~cmdline ~debug
+    | Init_effect.Success w -> w)
+
 let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path =
   (* Try to be sane w.r.t. \r\n in Windows *)
   Stdlib.set_binary_mode_in stdin true;

diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml
@@ -345,10 +345,16 @@ let version () =
   Format.asprintf "version %s, dev: %s, Coq version: %s" Version.server
     dev_version Coq_config.version
 
-let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug :
-    (string * Coq.Workspace.t) list =
-  match ifn () with
-  | Some (LSP.Message.Request { method_ = "initialize"; id; params }) ->
+module Init_effect = struct
+  type t =
+    | Success of (string * Coq.Workspace.t) list
+    | Loop
+    | Exit
+end
+
+let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
+  match msg with
+  | LSP.Message.Request { method_ = "initialize"; id; params } ->
     (* At this point logging is allowed per LSP spec *)
     let message =
       Format.asprintf "Initializing coq-lsp server %s" (version ())
@@ -363,17 +369,16 @@ let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug :
       List.map (fun dir -> (dir, Coq.Workspace.guess ~cmdline ~debug ~dir)) dirs
     in
     List.iter log_workspace workspaces;
-    workspaces
-  | Some (LSP.Message.Request { id; _ }) ->
+    Success workspaces
+  | LSP.Message.Request { id; _ } ->
     (* per spec *)
     LSP.mk_request_error ~id ~code:(-32002) ~message:"server not initialized"
     |> ofn;
-    lsp_init_loop ~ifn ~ofn ~cmdline ~debug
-  | Some (LSP.Message.Notification { method_ = "exit"; params = _ }) | None ->
-    raise Lsp_exit
-  | Some (LSP.Message.Notification _) ->
+    Loop
+  | LSP.Message.Notification { method_ = "exit"; params = _ } -> Exit
+  | LSP.Message.Notification _ ->
     (* We can't log before getting the initialize message *)
-    lsp_init_loop ~ifn ~ofn ~cmdline ~debug
+    Loop
 
 (** Dispatching *)
 let dispatch_notification ~ofn ~state ~method_ ~params : unit =

diff --git a/controller/lsp_core.mli b/controller/lsp_core.mli
@@ -30,12 +30,19 @@ end
 exception Lsp_exit
 
 (** Lsp special init loop *)
-val lsp_init_loop :
-     ifn:(unit -> Lsp.Base.Message.t option)
-  -> ofn:(Yojson.Safe.t -> unit)
+module Init_effect : sig
+  type t =
+    | Success of (string * Coq.Workspace.t) list
+    | Loop
+    | Exit
+end
+
+val lsp_init_process :
+     ofn:(Yojson.Safe.t -> unit)
   -> cmdline:Coq.Workspace.CmdLine.t
   -> debug:bool
-  -> (string * Coq.Workspace.t) list
+  -> Lsp.Base.Message.t
+  -> Init_effect.t
 
 (** Actions the scheduler requests to callers *)
 type 'a cont =