void set_name(const std::string & n) { name = n; }
void set_TeX_name(const std::string & n) { TeX_name = n; }
std::string get_name() const;
void set_name(const std::string & n) { name = n; }
void set_TeX_name(const std::string & n) { TeX_name = n; }
std::string get_name() const;