search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Add an option to control the printing panel #891

Open thomas-lamiaux opened 1 month ago

thomas-lamiaux commented 1 month ago

When you are writing in the code Print x then it prints it the definition in the proof window. However, when you are using Coq: Print it prints in the search panel added in VsCoq2. Would it be possible to choose where each prints ?

Typically, I would like to only print info in the proof goal if it is open as it already uses spaces on my screen and I would rather not have both.

thomas-lamiaux commented 1 month ago

Thinking about it maybe the proposition above is not the best for the underlying issue.

My issue is that the print view is very small compared to the previous VsCoq1 info. It is annoying as I often need to print and examine big terms.

Another possibility would be to be able to detach it like the goal tab. Or maybe to be able to make it full screen or sth ?

rtetley commented 1 month ago

The plan is too make the query panel detachable at some point. Or rather to add a button that will open the query panel in a normal buffer so the user can put it anywhere !