From b5c1f31aaa036717e02f67883e8ba033935b2029 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 6 Mar 2023 05:01:56 +0100
Subject: [PATCH] [coq] Don't expose feedback to clients.

This is unnecessary as init can hook directly with protect, and
should. No need to expose this internal detail.

This will simplify the setup in #433 (and other clients)
---
 controller/coq_lsp.ml | 26 +++-----------------------
 coq/init.ml           | 24 ++++++++++++++++++++----
 coq/init.mli          |  4 +---
 3 files changed, 24 insertions(+), 30 deletions(-)

diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index 31392c18e..d75382828 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -60,28 +60,10 @@ let lsp_cb =
           Lsp.JFleche.mk_progress ~uri ~version progress |> ofn)
     }
 
-let lvl_to_severity (lvl : Feedback.level) =
-  match lvl with
-  | Feedback.Debug -> 5
-  | Feedback.Info -> 4
-  | Feedback.Notice -> 3
-  | Feedback.Warning -> 2
-  | Feedback.Error -> 1
-
-let add_message lvl loc msg q =
-  let lvl = lvl_to_severity lvl in
-  q := (loc, lvl, msg) :: !q
-
-let mk_fb_handler q Feedback.{ contents; _ } =
-  match contents with
-  | Message (lvl, loc, msg) -> add_message lvl loc msg q
-  | _ -> ()
-
-let coq_init ~fb_queue ~debug =
-  let fb_handler = mk_fb_handler fb_queue in
+let coq_init ~debug =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
-  Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin })
+  Coq.Init.(coq_init { debug; load_module; load_plugin })
 
 let exit_notification =
   Lsp.Base.Message.(Notification { method_ = "exit"; params = [] })
@@ -111,10 +93,8 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path =
      initialize is received *)
 
   (* Core Coq initialization *)
-  let fb_queue = Coq.Protect.fb_queue in
-
   let debug = bt || Fleche.Debug.backtraces in
-  let root_state = coq_init ~fb_queue ~debug in
+  let root_state = coq_init ~debug in
   let cmdline =
     { Coq.Workspace.CmdLine.coqcorelib
     ; coqlib
diff --git a/coq/init.ml b/coq/init.ml
index 322852c37..7766223e8 100644
--- a/coq/init.ml
+++ b/coq/init.ml
@@ -19,14 +19,29 @@
 (**************************************************************************)
 
 type coq_opts =
-  { fb_handler : Feedback.feedback -> unit
-        (** callback to handle async feedback *)
-  ; load_module : string -> unit  (** callback to load cma/cmo files *)
+  { load_module : string -> unit  (** callback to load cma/cmo files *)
   ; load_plugin : Mltop.PluginSpec.t -> unit
         (** callback to load findlib packages *)
   ; debug : bool  (** Enable Coq Debug mode *)
   }
 
+let lvl_to_severity (lvl : Feedback.level) =
+  match lvl with
+  | Feedback.Debug -> 5
+  | Feedback.Info -> 4
+  | Feedback.Notice -> 3
+  | Feedback.Warning -> 2
+  | Feedback.Error -> 1
+
+let add_message lvl loc msg q =
+  let lvl = lvl_to_severity lvl in
+  q := (loc, lvl, msg) :: !q
+
+let mk_fb_handler q Feedback.{ contents; _ } =
+  match contents with
+  | Message (lvl, loc, msg) -> add_message lvl loc msg q
+  | _ -> ()
+
 let coq_init opts =
   (* Core Coq initialization *)
   Lib.init ();
@@ -40,7 +55,8 @@ let coq_init opts =
   (**************************************************************************)
 
   (* Initialize logging. *)
-  ignore (Feedback.add_feeder opts.fb_handler);
+  let fb_handler = mk_fb_handler Protect.fb_queue in
+  ignore (Feedback.add_feeder fb_handler);
 
   (* SerAPI plugins *)
   let load_plugin = opts.load_plugin in
diff --git a/coq/init.mli b/coq/init.mli
index 0a445bda6..12dded5ba 100644
--- a/coq/init.mli
+++ b/coq/init.mli
@@ -19,9 +19,7 @@
 (**************************************************************************)
 
 type coq_opts =
-  { fb_handler : Feedback.feedback -> unit
-        (** callback to handle async feedback *)
-  ; load_module : string -> unit  (** callback to load cma/cmo files *)
+  { load_module : string -> unit  (** callback to load cma/cmo files *)
   ; load_plugin : Mltop.PluginSpec.t -> unit
         (** callback to load findlib packages *)
   ; debug : bool  (** Enable Coq Debug mode *)