Yes, if you do it on top of the lexer it starts to make sense to me. I still think the language should also support the corresponding "ligatures", so that no co

Yes, if you do it on top of the lexer it starts to make sense to me. I still think the language should also support the corresponding "ligatures", so that no confusion can result if you happen to enter ≤ directly, but this is actually a nice solution to the problem of what to do in your language aware editor when the user enters <= : nothing! You just assign to different token classes different fonts.