Incorrect environment in command snaps for code action

[digama0]

import Lean
open Lean Server

@[code_action_provider] def holeCodeActionProvider : CodeActionProvider := fun _ snap => do
  panic! toString <| snap.cmdState.env.contains `foo
  pure #[]

def foo : Nat := 
  -- here
  1

Placing the cursor at the indicated location results in true being printed, meaning that the environment passed in the snap corresponds to the one after the command is executed. This results in incorrect behavior when traversing the info trees, because unless the environment is overridden in the context info it will still say that we are in the new environment, not the original environment used for the actual elaboration. I believe this issue was preexisting but exacerbated by #3159, because previously all info tree context nodes would override the environment and now most of them don't.

This is causing problems for the implementation of leanprover-community/batteries#577 , which needs to be able to determine whether an instance exists prior to the command to mimic the behavior of the structure instance notation.