Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[infoview] Show notices on panel instead of diagnostics #125

Closed
ejgallego opened this issue Dec 27, 2022 · 0 comments · Fixed by #128 or ocaml/opam-repository#22861
Closed

[infoview] Show notices on panel instead of diagnostics #125

ejgallego opened this issue Dec 27, 2022 · 0 comments · Fixed by #128 or ocaml/opam-repository#22861
Labels
kind: enhancement New feature or request part: client (VSCode) part: goals and info panel part: lsp server part: protocol (LSP)
Milestone
0.1.2

Comments

@ejgallego
Copy link
Owner

As of today, we show Coq's feedback Notice using diagnostics. This includes Search, Check, etc...

This is not good in most cases, instead, make that optional, and show them instead as messages in the goal / info panel.
@ejgallego ejgallego added this to the 0.1.2 milestone Dec 27, 2022
ejgallego added a commit that referenced this issue Dec 27, 2022
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
d9b90bb 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
@ejgallego ejgallego mentioned this issue Dec 27, 2022
Merged
ejgallego added a commit that referenced this issue Dec 27, 2022
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
450fe85 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
ejgallego added a commit that referenced this issue Dec 27, 2022
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
379f40a 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
ejgallego added a commit that referenced this issue Dec 27, 2022
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
2798066 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
ejgallego added a commit that referenced this issue Jan 3, 2023
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
5e13a24 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
ejgallego added a commit that referenced this issue Jan 3, 2023
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
ed5f83e 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
ejgallego added a commit that referenced this issue Jan 3, 2023
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
f8757ea 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
ejgallego added a commit that referenced this issue Jan 3, 2023
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
de54763 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
ejgallego added a commit that referenced this issue Jan 3, 2023
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
6199ba7 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
ejgallego added a commit that referenced this issue Jan 4, 2023
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
74ae6ab 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

A configuration option allows to restore old behavior.

Fixes #125
ejgallego added a commit that referenced this issue Jan 4, 2023
@ejgallego
[infoview] Show Notice feedbacks on panel instead of as diagnostics
a4eeafa 
This seems more sensible as Coq (legacy) will produce large amounts of
these kind of Coq messages when for example `Search` or `About` is
used.

Thus, users can click on the concrete command and obtain the messages
information in the side panel; moreover, this allows for better
rendering opportunities.

We also implement a detailed display for errors, as Coq errors can be
large and don't fit properly in the diagnostics list.

A configuration option allows to restore old behavior.

Fixes #125
@ejgallego ejgallego mentioned this issue Jan 5, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Jan 6, 2023
@ejgallego
[new release] coq-lsp (0.1.2+v8.16)
7923d13 
CHANGES:

------------------------

 - Send an error to the client if the client and server versions don't
   match (@ejgallego, ejgallego/coq-lsp#126)
 - Parse options -noinit, -indices-matter, and -impredicative-set from
   `_CoqProject` (@artagnon, @ejgallego, ejgallego/coq-lsp#140, ejgallego/coq-lsp#150)
 - Log file `log-lsp.txt` has been removed in favor of `coq-lsp.trace.server`
   (@artagnon, @ejgallego, ejgallego/coq-lsp#130, ejgallego/coq-lsp#148)
 - Added --bt flag to print a backtrace on error (@Alizter, ejgallego/coq-lsp#147)
 - A detailed view of Coq errors is now displayed in the info panel
   (@ejgallego, ejgallego/coq-lsp#128)
 - Coq "Notice" messages, such as the ones generated by `About` or
   `Search` are not shown anymore as diagnostics. Instead, they will
   be shown on the side panel when clicking on the corresponding
   command. The `show_notices_as_diagnostics` option allows to restore
   old behavior (@ejgallego, ejgallego/coq-lsp#128, fixes ejgallego/coq-lsp#125)
 - Print some more info about Coq workspace configuration (@ejgallego, ejgallego/coq-lsp#151)
 - Admit failed `Qed` by default; allow users to configure it
   (@ejgallego, ejgallego/coq-lsp#118, fixes ejgallego/coq-lsp#90)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement New feature or request part: client (VSCode) part: goals and info panel part: lsp server part: protocol (LSP)
Projects
None yet
Milestone
0.1.2
1 participant
@ejgallego