Merge pull request #451 from ejgallego/fb_internal_to_coq

[coq] Don't expose feedback to clients.

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

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

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 *)