[lsp] Connect LSP message to actual JsCoq Log worker event.

jscoq · Aug 9, 2023 · 7c0475f · 7c0475f
1 parent e8270f3
commit 7c0475f
Showing 1 changed file with 9 additions and 1 deletion.
diff --git a/backend/common/jscoq_interp.ml b/backend/common/jscoq_interp.ml
@@ -100,11 +100,19 @@ let mk_vo_path l = Jslib.paths_to_coqpath ~implicit:!opts.implicit_libs l
 let cur_workspace = ref None
 let root_state = ref (Coq.State.of_coq (Vernacstate.freeze_interp_state ~marshallable:false))
 
+let lvl_to_fb = function
+  | 0 -> Feedback.Error
+  | 1 -> Feedback.Warning
+  | 2 -> Feedback.Notice
+  | 3 -> Feedback.Info
+  | 4 -> Feedback.Debug
+  | _ -> Feedback.Debug
+
 let lsp_cb =
   let out_fn = post_answer in
   Fleche.Io.CallBack.
     { trace = (fun cat ?extra:_ msg -> Format.eprintf "[%s] %s@\n%!" cat msg)
-    ; message = (fun ~lvl:_ ~message:_ -> ())
+    ; message = (fun ~lvl ~message -> out_fn (Log (lvl_to_fb lvl, Pp.str message)))
     ; diagnostics = (fun ~uri ~version diagnostic ->
           out_fn (Notification { uri; version; diagnostic }))
     ; fileProgress = (fun ~uri:_ ~version:_ _progress -> ())