Tope highlighting captures more than it should

[fredrik-bakke]

In the following example, the tope highlighting is quite inaccurate and in particular captures parentheses it shouldn't, interfering with the rainbow parentheses function of vscode:

Code

#def fubini
  ( I J : CUBE)
  ( ψ : I -> TOPE)
  ( ϕ : ψ -> TOPE)
  ( ζ : J -> TOPE)
  ( χ : ζ -> TOPE)
  ( X : ψ -> ζ -> U)
  ( f : { (t , s) : I * J | (ϕ t /\ ζ s) \/ (ψ t /\ χ s)} -> X t s )
  : Equiv
    ({t : I | ψ t} -> ({ s : J | ζ s} -> X t s [ χ s |-> f (t , s) ]) [ ϕ t |-> \{s : J | ζ s} -> f (t , s) ])
    ({s : J | ζ s} -> ({ t : I | ψ t} -> X t s [ ϕ t |-> f (t , s) ]) [ χ s |-> \{t : I | ψ t} -> f (t , s) ])
  :=
    comp-equiv
      ({t : I | ψ t} -> ({ s : J | ζ s} -> X t s [ χ s |-> f (t , s) ]) [ ϕ t |-> \{s : J | ζ s} -> f (t , s) ])
      ({ (t , s) : I * J | ψ t /\ ζ s} -> X t s [(ϕ t /\ ζ s) \/ (ψ t /\ χ s) |-> f (t , s)])
      ({s : J | ζ s} -> ({ t : I | ψ t} -> X t s [ ϕ t |-> f (t , s) ]) [ χ s |-> \{t : I | ψ t} -> f (t , s) ])
      (curry-uncurry I J ψ ϕ ζ χ X f)
      (uncurry-opcurry I J ψ ϕ ζ χ X f)

[fizruk]

This seems to be a problem in the TextMate grammar. I think it incorrectly handles nested extension types.