diff --git a/CHANGES.md b/CHANGES.md index fb690565a..19e994b14 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -39,6 +39,8 @@ - URI validation is now more strict, and some further bugs should be solved; note still this can be an issue on some client settings (@ejgallego, #313, fixes #187) + - Display Coq info and debug messages in info panel (@ejgallego, + #314, fixes #308) # coq-lsp 0.1.4: View --------------------- diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 30911be38..355df2879 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -115,12 +115,7 @@ let add_message lvl loc msg q = let mk_fb_handler q Feedback.{ contents; _ } = match contents with - | Message (((Error | Warning | Notice) as lvl), loc, msg) -> - add_message lvl loc msg q - | Message ((Info as lvl), loc, msg) -> - if !Fleche.Config.v.show_coq_info_messages then add_message lvl loc msg q - else () - | Message (Debug, _loc, _msg) -> () + | Message (lvl, loc, msg) -> add_message lvl loc msg q | _ -> () let coq_init ~fb_queue ~debug = diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index e1517bb35..2acc8efc8 100644 --- a/controller/rq_goals.ml +++ b/controller/rq_goals.ml @@ -6,7 +6,13 @@ (************************************************************************) (* Replace by ppx when we can print goals properly in the client *) -let mk_message (_loc, _lvl, msg) = msg +let mk_message (_loc, lvl, msg) = + let hdr = + if lvl = 4 then Pp.str "[info ] " + else if lvl = 5 then Pp.str "[debug] " + else Pp.mt () + in + Pp.(hdr ++ msg) let mk_messages node = Option.map Fleche.Doc.Node.messages node diff --git a/editor/code/views/info/media/messages.css b/editor/code/views/info/media/messages.css index e69de29bb..3486eb462 100644 --- a/editor/code/views/info/media/messages.css +++ b/editor/code/views/info/media/messages.css @@ -0,0 +1,3 @@ +ul.messageList { + padding-inline-start: 1em; +} diff --git a/fleche/doc.ml b/fleche/doc.ml index 5c7f48d03..2edfe26a8 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -32,11 +32,14 @@ module Util = struct mk_diag range severity message let diags_of_messages ~drange fbs = - let diags, messages = List.partition (fun (_, lvl, _) -> lvl < 3) fbs in - let diags = - if !Config.v.show_notices_as_diagnostics then - diags @ List.filter (fun (_, lvl, _) -> lvl = 3) fbs - else diags + (* TODO, replace this by a cutoff level *) + let cutoff = + if !Config.v.show_coq_info_messages then 5 + else if !Config.v.show_notices_as_diagnostics then 4 + else 3 + in + let diags, messages = + List.partition (fun (_, lvl, _) -> lvl < cutoff) fbs in (List.map (feed_to_diag ~drange) diags, messages)