Notation `x[...]'...` gets confused with a character literal

[Rob23oba]

Description

Indexing notation with proof is sometimes mistaken with a character literal, which can cause formatting to look weird later:

Context

I discovered this while working on hash map code:
leanprover/lean4#7400 (comment)

Steps to Reproduce

@[simp]
def foo (x : Array Nat) (i : Nat) (h' : i < x.size) :
    0 ≤ x[i]'h' :=
  Nat.zero_le _

@[simp]
def bar (x : Array Nat) (i' : Nat) (h : i' < x.size) :
    0 ≤ x[i']'h :=
  Nat.zero_le _

@[simp]
def baz : 2 = 2 := rfl

Expected behavior:
The [...] should be detected as a closed pair of brackets, the ' afterwards shouldn't get any special formatting.

Actual behavior:
In the first case, the [..] is detected as closed pair of brackets; however, the ' afterwards gets highlighted like a character literal, the remainder of the "character literal" is overriden by the semantic highlighting information from the server.
In the second case it treats [ as unclosed and ']' as a character literal (although the first quote gets again overriden by semantic highlighting). Due to fact that it treats [ as unclosed, the remainder has slightly wrong highlighting, e.g. @[simp] in baz isn't recognized as an attribute.

Versions

Version 0.0.202

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.