+ } else if (p.next_token().asInput() == "\\ascii") {
+ // handle the \ascii characters
+ // (the case without braces is handled later)
+ // the code is "{\ascii\xxx}"
+ p.get_token(); // eat \ascii
+ string name2 = p.get_token().asInput();
+ p.get_token(); // eat the final '}'
+ string const name = "{\\ascii" + name2 + "}";
+ bool termination;
+ docstring rem;
+ set<string> req;
+ // get the character from unicodesymbols
+ docstring s = encodings.fromLaTeXCommand(from_utf8(name),
+ Encodings::TEXT_CMD, termination, rem, &req);
+ if (!s.empty()) {
+ context.check_layout(os);
+ os << to_utf8(s);
+ } else
+ // we did not find a non-ert version
+ output_ert_inset(os, name, context);
+ continue;