fix: make VsCoq activity bar logo appear only when Coq files present

[Durbatuluk1701]

This adds a context to watch and track the presence of Coq files in the current workspace, and will dynamically display the activity bar logo only if Coq files are present.

Should fix coq-community/vscoq#886

[Durbatuluk1701]

@rtetley Pushed two commits: The first one is a more robust approach where if all Coq-related files are deleted then the activity bar logo disappears. The second one does not care about making the activity bar logo disappear if all Coq-related files are deleted.

Both include adding a language entry for _CoqProjects. This allows for proper comment toggling in CoqProjects via the VsCode built in commenting command (ctrl + k + (c | u) for me), as well as providing syntax highlighting. Importantly it also allows for an implicit onLanguage:coq-project activation event so that anytime someone creates/opens a CoqProject file, the extension will be activated if it is not already.

Let me know your thoughts on the CoqProject language entry, and which of the two commit methods seem more reasonable to you.

[rtetley]

I like this very much ! I was worried about _CoqProject comments being parsed anyways because of https://github.com/coq-community/vscoq-legacy/issues/49 but it turns out after checking that we do ignore comments ! I'm not sure what we should do about visibility. I think making it disappear is actually fine since it makes little sense to use the activity bar when there are no coq files present.

[Durbatuluk1701]

I'm not sure what we should do about visibility. I think making it disappear is actually fine since it makes little sense to use the activity bar when there are no coq files present.

Sounds good, pushed changes to make it appear/disappear on file create/delete if it should

[rtetley]

Ah I would much rather you rebase onto main. Do you mind resetting to https://github.com/coq-community/vscoq/pull/897/commits/455b5f1cbd1c0637ac3ba9266aa520af6b64a191 then rebasing on main ?

[Durbatuluk1701]

Yes sorry, I didn't know that using the GitHub built in conflict resolution made a merge

[Durbatuluk1701]

Unrelated to this PR but I didn't know where else to ask; is it intended that v2.2.0 release is not on the vscode marketplace yet @rtetley

[rtetley]

I am waiting for https://github.com/ocaml/opam-repository/pull/26506#issuecomment-2346070468

In general I like to sync the release of the language server and the extension. In this case I suppose it's not blocking but I could be confusing.

[Durbatuluk1701]

I am waiting for ocaml/opam-repository#26506 (comment)

In general I like to sync the release of the language server and the extension. In this case I suppose it's not blocking but I could be confusing.

That makes perfect sense and is a good practice. I was mainly just curious

[RalfJung]

Thanks for implementing this!

So what will the behavior of the icon be then?

The LaTeX workshop icon only appears when I actually open a tex file. That's quite nice as it means if a workspace happens to contain a tex file I don't care about, I don't have the icon clutter the sidebar. But the discussion above makes it sound like the Coq icon will appear whenever a Coq file exists, even if no Coq file is ever opened?

[Durbatuluk1701]

Thanks for implementing this!

So what will the behavior of the icon be then?

The LaTeX workshop icon only appears when I actually open a tex file. That's quite nice as it means if a workspace happens to contain a tex file I don't care about, I don't have the icon clutter the sidebar. But the discussion above makes it sound like the Coq icon will appear whenever a Coq file exists, even if no Coq file is ever opened?

@RalfJung you are correct, it would function based on if the active workspace is related to Coq (existence of a Coq related file), not the specific focused or opened file(s).

I can definitely see the use case you are describing (and it would be programmatically easier to implement). I feel like it sort of comes down to preference, I personally dislike my sidebar changing much once the workspace is loaded.

I think maybe we should think of the following possible cases and spec out what would be optimal behavior for the activity bar:

Here is its current behavior (feel free to add any more conditions that might be relevant):	Condition	Activity Bar Displayed
*.v file exists in the workspace	True
_CoqProject file exists in the workspace	True
*.v file is open	True
_CoqProject file is open	True
*.v file is focused	True
_CoqProject file is focused	True

[RalfJung]

I feel like it sort of comes down to preference, I personally dislike my sidebar changing much once the workspace is loaded.

Yeah that's fair. I think I have exactly one workspace that contains .v files I don't want it to open (since I have a separate sub-workspace for that folder)... so not worth a lot of effort, I just figured I would bring this up.

[Durbatuluk1701]

We could add a config option along the lines of vscoq.proof.displayActivityBar = FocusedFile | Workspace then modify the when clause to be: (vscoq.proof.displayActivityBar == FocusedFile && resourceLangId == coq) || (vscoq.proof.displayActivityBar == Workspace && inCoqProject)

With Workspace mode it would work as I mentioned above.

With FocusedFile mode it would work as:	Condition	Activity Bar Displayed
*.v file exists in the workspace	False
_CoqProject file exists in the workspace	False
*.v file is open	False
_CoqProject file is open	False
*.v file is focused	True
_CoqProject file is focused	False

[TheoWinterhalter]

Do people actually use the sidebar though? One of the first things I did when configuring VSCode was getting rid of it given how useless it is, am I missing on anything?

[Durbatuluk1701]

Do people actually use the sidebar though? One of the first things I did when configuring VSCode was getting rid of it given how useless it is, am I missing on anything?

Like in general or specifically for VsCoq? I like the vscode provided workspace search and source control built into the sidebar and use it fairly frequently. The VsCoq one I do not use because I'd rather type my Search, Check, etc. commands in a file and have them print in the proof view.

[TheoWinterhalter]

I see, thanks. I do use those features but using commands. It's good to have it at least for new users I guess. :)