OK, I played with the colors for (3) a bit more - basically, we have 2 choices - either dim the red a little or go towards the orange color. The original color `#7f0000` was basically the dimmed red and to avoid user shock from different colors, I would rather go this direction (the orange is a bit too flashy to my liking). As you mentioned, it might not be red enough to distinguish from grey so I added a little more red and the result is `#cc4033` but I think I wouldn't add more red than that, it then becomes hard to distinguish from the error red.
So the colors would be: 1. `#006eff` 2. `#009000` - after playing with it, made it a little darker than what I suggested before 3. `#cc4033` 4. `#ff0000` - the original red (also used in the editor to underline errors so these should be the same)
The colors are a little on the darker side in dark themes but still usable and I don't want to make the colors much worse for light themes which I think more users still use so I prioritized contrast for light themes with the colors.
I guess it's impossible to find perfect colors, you can always find some backgrounds for which it doesn't work. Also, maybe I have a little too good monitor for this - but I tried with an external monitor which is worse than the one on the MacBook and these colors seem to be OK there too.