Skip to content

Commit

Permalink
[messages] Print warnings in info panel
Browse files Browse the repository at this point in the history
Fixes #195
  • Loading branch information
ejgallego committed Feb 14, 2023
1 parent 0d95d5c commit 5c5747e
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 3 deletions.
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,8 @@
will now be properly represented, as well as constructors for
inductive types, projections for records, etc... (@ejgallego,
#174, fixes #121, #122)
- Warnings are not printed in the info view messages panel
(@ejgallego, #, fixes #195)

# coq-lsp 0.1.4: View
---------------------
Expand Down
7 changes: 4 additions & 3 deletions controller/rq_goals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,12 @@
(* Replace by ppx when we can print goals properly in the client *)
let mk_message (_loc, lvl, msg) =
let hdr =
if lvl = 4 then Pp.str "[info ] "
else if lvl = 5 then Pp.str "[debug] "
if lvl = 2 then Pp.str "[warning] "
else if lvl = 4 then Pp.str "[info ] "
else if lvl = 5 then Pp.str "[debug ] "
else Pp.mt ()
in
Pp.(hdr ++ msg)
Pp.(hdr ++ hov 0 msg)

let mk_messages node =
Option.map Fleche.Doc.Node.messages node
Expand Down
2 changes: 2 additions & 0 deletions fleche/doc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@ module Util = struct
let diags, messages =
List.partition (fun (_, lvl, _) -> lvl < cutoff) fbs
in
let warnings = List.filter (fun (_, lvl, _) -> lvl = 2) fbs in
let messages = warnings @ messages in
(List.map (feed_to_diag ~drange) diags, messages)

let build_span start_loc end_loc =
Expand Down

0 comments on commit 5c5747e

Please sign in to comment.