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 #886

[rtetley]

Thanks for this !

[rtetley]

I think you can replace this by the "workspaceContains" activation event in the package.json (see here). I am not sure if it requires workspace capabilities from the server that we still need to implement but I don't see why.

[Durbatuluk1701]

I think it would be cool to use the activation event, the only downsides I can think of are:

• The workspaceContains is only emitted on folder open (not file creation or deletion). For example, this would make it so if we open an new/empty folder, then create a _CoqProject it won't make the activity bar entry appear
  (this could maybe mitigated by adding _CoqProject to the recognized extensions for the coq language, although I think this would involve more separate work)

• Similarly to above, since no deletion events are tracked the activity bar entry wont disappear if all .v and _CoqProject files disappear. This does seem like a corner case though, if someone ends up deleting all their Coq related files they can maybe deal with the activity bar entry sticking around.

[rtetley]

Okay ! I see your point ! I think it is fine as is then ! Could you just add _CoqProject as part of the checkCoqFilesPresent() routine ? I'll then merge !

[rtetley]

If you use the activation event this simply can be replaced by a

commands.executeCommand('setContext', 'coqFilesPresent', true);

Don't forget to "deset" it in the deactivate function, i.e. add

commands.executeCommand('setContext', 'coqFilesPresent', undefined);

in the deactivate function

[rtetley]

I suppose on top of that, it could activate if other files are present such as a _CoqProject file ?
So maybe call the context 'inCoqProject' ?

[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 coq-community/vscoq-legacy#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]

Thanks !

[rtetley]

Ah I would much rather you rebase onto main. Do you mind resetting to 455b5f1 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 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.

[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. :)