VSCode PullRequest extension

Stream: general

[Filippo A. E. Nuccio]

I like and often use the VSCode Pull Request extension but there is something I do not understand: when I open the left-panel and see all files that have been changed in the PR, some of them are marked with a small :cloud: (which I ended up understanding as "there are some comments"), and some are marked with a letter, typically either A, M, R (and perhaps others that I haven't met yet). What do these letters mean?

[Johan Commelin]

A = add?, M = move?, R = remove?

Just guessing

[Filippo A. E. Nuccio]

:thinking: It could be, I thought they were more related to the discussion (like Answered, Reviewed, M...?)

[Filippo A. E. Nuccio]

(of course, if someone has a link to a doc, I'd be more than happy :smile: )

[Filippo A. E. Nuccio]

Filippo A. E. Nuccio said:

:thinking: It could be, I thought they were more related to the discussion (like Answered, Reviewed, M...?)

Well, actually in the PR I am reviewing your guess is 100% accurate. :100:

[Pietro Monticone]

Those capitalized letters in the file explorer are git status badges indicating the type of change that has been made on each file.

In particular:

• “A” stands for “added”
• “M” stands for “modified”
• “D” stands for “deleted”
• “R” stands for “renamed”
• “U” stands for “untracked”

For further details you can check directly the VSCode Git extension API here using “status” and “gitDecoration” as keywords or take a look at issues like this one.

[Filippo A. E. Nuccio]

Thanks!

[Filippo A. E. Nuccio]

And (completely unrelated) do you know how to automatically lock the editor group containing the Infoview? There is the option of locking an editor "matching a type" and there are 18 proposed types: I wonder wether the infoview's belongs to one of these types.

[Marc Huisinga]

Filippo A. E. Nuccio said:

And (completely unrelated) do you know how to automatically lock the editor group containing the Infoview? There is the option of locking an editor "matching a type" and there are 18 proposed types: I wonder wether the infoview's belongs to one of these types.

I've looked into this briefly, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/InfoView.20focus.20issue/near/439194251.

[Filippo A. E. Nuccio]

Gorgeuous, thanks!