+ // matching entry in the unicodesymbols file.
+ // If the entry doesn't start with '\', we take note
+ // of the match and continue (this is not a ultimate
+ // acceptance, as some other entry may match a longer
+ // portion of the cmd string). However, if the entry
+ // does start with '\', we accept the match only if
+ // this is a valid macro, i.e., either it is a single
+ // (nonletter) char macro, or nothing else follows,
+ // or what follows is a nonletter char, or the last
+ // character is a }.