+std::string symbol::get_name() const
+{
+ if (name.empty()) {
+ name = "symbol" + std::to_string(serial);
+ }
+ return name;
+}
+
+std::string symbol::get_TeX_name() const
+{
+ if (TeX_name.empty()) {
+ return get_default_TeX_name(get_name());
+ }
+ return TeX_name;
+}
+
+// protected
+