server sync bug in syntax quotations

MWE:

import Lean

elab (ident)? ("Foo") : command => sorry

syntax "Fix " colGt ident : tactic

example (x : Lean.TSyntax `ident) : Lean.MacroM Lean.Syntax :=
  `(tactic| Fix $x:iden)
                    -- ^ insert a 't' here

As written, the example produces three parse errors, on the $, the : and the ). Inserting t to complete the word ident makes the example correct (which can be confirmed by compiling on the command line), but in the server it continues to report errors on the $ and the ). Removing and re-adding :ident makes the error go away, and removing and re-adding ident makes it come back.

Tested on leanprover/lean4:v4.9.0-rc3.

Start with the reported Lean MWE and compare command-line compilation with the server's diagnostics after completing ident in the syntax quotation. Investigate why removing and re-adding :ident changes the reported errors; done means the server matches command-line behavior and clears the stale parse errors without requiring text edits.