[VsCoq1] Added a rudimentary message panel

[zqy1018]

Tried implementing a rudimentary message panel in the fashion of that in CoqIDE. Also including some modifications on the displaying style (see html_views/src/goals/proof-view.css).

Screenshots:

Features:

• Output is highlighted (rendered using the same utilities of rendering goals/hypotheses)
• Per-document (each document holds its own message panel, just like the proof view)
• Searchable (with the search widget provided by the webview, see Line 154 in client/src/HtmlCoqView.ts)

Some known issues:

• Not resizable (don't know how to implement it 😥)
• Only show the responses of queries triggered by commands like Coq: Search (possibly can be resolved by adding more panels and substituting them for the output channels)

Technical details:

• Added another vscode-panel-view showing messages (from vscode-webview-ui-toolkit) below the proof view
• Messages are passed from the client on receiving them, using the extended CommandResult type (see the two changed protocol.ts)

[Blaisorblade]

Hi, thank you for your proposal! I haven't yet tried your MR but from your description I have a question: What would you propose to do with the existing message panel at the editor's bottom? The highlighting is a clear upside, but I wonder if having both could be confusing?

The existing panel supports multiple log levels, not just Query — but I recall some people suggested having a combined view.

[zqy1018]

Thank you for the comment. Yes, it seems that the existing message panels in the OUTPUT tab can be disabled now, and this can be achieved by removing the code in client/src/CoqDocument.ts. For example:

For the combined view, I suppose it can be achieved by somehow relaying all output messages to the new message panel. For example, relaying all messages originally shown in the Notices channel to the new message panel (without clearing every time):

Or, add more panels beside the QUERY panel and relay the output from channels to their respective panels:

[zqy1018]

Some update:

• Now there is only one combined message panel, and all output channels at the editor's bottom are removed (by commenting out all related code)
• The message panel is cleared on demand (if there is no new message coming, then the message panel will not be cleared)

I did some simple local testing and it seems to work fine. Example:

[Blaisorblade]

I'm sorry I haven't had time to take a look, but I remember talking with @MSoegtropIMC (and others) about how the dialog should best work?

We should also assign somebody to review the code a bit — @thery, @huynhtrankhanh, do you think you could do that at some point, or would know who could? Without an expert reviewer, we should be willing to merge this after some testing.

[Blaisorblade]

@zqy1018 BTW, do you have a fix for the conflict? If you haven't yet, we should probably test and review your branch.

[zqy1018]

Conflict fixed. Now each query result will be either displayed as hovering text (due to the newly added hovering provider) or sent to the message panel.

@Blaisorblade I found this Topic on Zulip to which I suppose you are referring. In summary, maybe the following features are desirable:

• a unified and resizable message panel, with an option to allow it either showing the entire query history, or only showing the last query result
• each query result should be accompanied with some meta-data (e.g., the query command)
• whenever multiple query results are shown, they should be separated with certain separators
• the message panel should scroll to its bottom automatically when a new result comes

[Blaisorblade]

@Blaisorblade I found this Topic on Zulip to which I suppose you are referring.

Great sleuthing, that's the thread :-)

[huynhtrankhanh]

Not resizable

I can help implement this. You could focus on improving other aspects of the PR.

This is important work as this PR vastly improves the user experience of VsCoq.

[dlesbre]

I've experimented with this a bit and do indeed find it fairly useful ! I'd like to add a few things to the list of requirements though :

• Make the panel searchable. I'm not sure why, while VS Code does allow me to open a search window in the proofView/message panel, it doesn't seem capable of actually doing the search. This feature worked well in the old query panel and I found it rather useful when a Coq Search command can return hundreds of results.
• Ideally, when showing multiple queries with separators, the separators could have buttons to fold or clear their section. As, once again, query results can be very long.

[huynhtrankhanh]

Wait. https://github.com/microsoft/vscode-webview-ui-toolkit/blob/main/src/divider/README.md

There must be a good reason behind this rule. Right now, we are abusing the divider to split the proof view into two pseudoviews. And if the official documentation says we shouldn't, maybe this means we are supposed to create a new webview for this. And thus we won't need to implement resizing ourselves. Well, it's not like implementing resizing ourselves is very hard to do, but the question is whether this is the right course of action.

Right now, this is a cute prototype, but we need careful consideration.

[thery]

what is the status of this PR?

[zqy1018]

Sorry, I have not been able to work on the pull request since I started grad school, and my current circumstances may prevent me from picking it up in the near future. 😢 I would greatly appreciate it if someone could take it forward!