coq-community
Automatically switching ProofView tab
Hello all,
When I switch to a different Coq file, ProofView tab isn't automatically switched to the corresponding one. Is there any option or any plan for supporting this?
VSCoq is a great plugin. Thank you for your maintenance!
Thanks for reporting. #143 improves the situation, by switching to the right proofview when a step is performed. Once we have #140, we could completely close this issue by switching the proofview when a file is opened.
FWIW: after using #143 for a while, I think it's a regression. Sometimes overriding the choices becomes impossible. In particular, while stepping through a proof on the left pane, it becomes impossible to view a different file on the right pane.
With the right keycombo, switching by hand is easy enough; if that's a burden, VsCoq could make it easier (e.g. by adding a command for it). https://github.com/coq-community/vscoq/issues/144#issuecomment-642551449
Hi, Maybe we can have an option that turns it on/off? I also frequently open a different file on the right pane when skimming over definitions and writing functions rather than proving something. I'd like to try the latest version of VSCoq (the one that #143 is applied). What is the good way to do it? My VSCode isn't showing its latest version. :/
#143 was applied, but I find it an extremely strong regression, without a way to override it. Especially because the autofocus triggers without actually stepping through a proof.
This is still a problem, and @thery might have asked about this in https://github.com/coq-community/vscoq/pull/327:
Another question, when I have several ProofView, I'd like that the one that receives a new goal to be visible. What is the proper way to do this?
The present issue has some history on this: I think we fixed that a while ago, but reverted the fix (in part because of me)... https://github.com/coq-community/vscoq/issues/144 links to https://github.com/coq-community/vscoq/pull/143 and https://github.com/coq-community/vscoq/pull/82.
These days I'd like at least a shortcut to open the matching proof view in one step...
@Blaisorblade I have been testing #143 and it seems the right behavior to me. I am not sure I understood what was troubling you. The switches seem to happen when there are new infos on the proof window, so it seems ok
