Skip to content

Commit

Permalink
[messages] Enable display of info and debug messages.
Browse files Browse the repository at this point in the history
Fixes #308

We delay the resolution of #195 as the UI story for duplicating
information is still not very clear.
  • Loading branch information
ejgallego committed Feb 13, 2023
1 parent c1f9736 commit ab8134b
Show file tree
Hide file tree
Showing 5 changed files with 21 additions and 12 deletions.
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
---------------------
Expand Down
7 changes: 1 addition & 6 deletions controller/coq_lsp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
8 changes: 7 additions & 1 deletion controller/rq_goals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions editor/code/views/info/media/messages.css
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
ul.messageList {
padding-inline-start: 1em;
}
13 changes: 8 additions & 5 deletions fleche/doc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down

0 comments on commit ab8134b

Please sign in to comment.