vscoq icon indicating copy to clipboard operation
vscoq copied to clipboard

Print Notices/Error messages etc. in same buffer

Open Alizter opened this issue 2 years ago • 5 comments

Similar to how to CoqIDE prints information, we should print all information in a buffer which refreshes on each print. We can also have another log of all past messages (or separate them if need be). But it is very confusing at the moment to switch between Notices etc.

Alizter avatar Mar 07 '22 12:03 Alizter

To demonstrate how broken things are currently, when doing something like:

Fail Check (Set : Set).

Doesn't output anywhere I can find.

Alizter avatar Mar 07 '22 17:03 Alizter

Odd, for me it opens directly the "Notice" panel (was closed before) and prints:

The command has indeed failed with message:
In environment
state : Type
The term "Set" has type "Type" while it is expected to have type 
"Set" (universe inconsistency: Cannot enforce Set+1 <= Set).

which I think is the expected behaviour.

TheoWinterhalter avatar Mar 07 '22 17:03 TheoWinterhalter

Hmm it seems to be working now that I restarted VSCoq. I am not sure what happened there.

Alizter avatar Mar 07 '22 17:03 Alizter

Anyway, my point still stands. We should have a buffer that collects all of these and shows the newest and make that the default.

Alizter avatar Mar 07 '22 17:03 Alizter

Adding this to the VsCoq 2 road map as it doesn't seem to work.

rtetley avatar Sep 04 '23 08:09 rtetley