else if(i->get_signature()==FloatType::signature)
out.write(format("%15g", (i->get<FloatType::Store>())));
else if(i->get_signature()==SymbolType::signature)
- out.write(i->get<SymbolType::Store>().name);
+ {
+ string name = i->get<SymbolType::Store>().name;
+ if(isdigit(name[0]))
+ out.write("\\"+name);
+ else
+ out.write(name);
+ }
}
if(!st.sub.empty())
{