- name_ == "overline" ||
- name_ == "underline" ||
- name_ == "overbrace" ||
- name_ == "underbrace" ||
- name_ == "overleftarrow" ||
- name_ == "overrightarrow" ||
- name_ == "overleftrightarrow" ||
- name_ == "widehat" ||
- name_ == "widetilde" ||
- name_ == "underleftarrow" ||
- name_ == "underrightarrow" ||
- name_ == "underleftrightarrow";
+ key_->name == "overline" ||
+ key_->name == "underline" ||
+ key_->name == "overbrace" ||
+ key_->name == "underbrace" ||
+ key_->name == "overleftarrow" ||
+ key_->name == "overrightarrow" ||
+ key_->name == "overleftrightarrow" ||
+ key_->name == "widehat" ||
+ key_->name == "widetilde" ||
+ key_->name == "underleftarrow" ||
+ key_->name == "underrightarrow" ||
+ key_->name == "underleftrightarrow";