michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean): fix some output of escaped identifiers

Browse source
This commit is contained in:
Sebastian Ullrich 2016-08-25 10:08:40 -04:00
parent a086fb3348
commit d7320f4938
2 changed files with 15 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/parser.cpp
View file

@ -194,7 +194,7 @@ void parser::scan() {
ok = false;
}
if (!ok)
m_ios.get_regular_stream() << "unknown identifier '" << id << "'\n";
m_ios.get_regular_stream() << "unknown identifier '" << id.escape() << "'\n";
print_lean_info_footer(m_ios.get_regular_stream());
m_info_at = false;
}
@ -1561,7 +1561,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
}
}
if (!r)
throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
throw parser_error(sstream() << "unknown identifier '" << id.escape() << "'", p);
save_type_info(*r);
if (is_constant(*r)) {
add_ref_index(const_name(*r), p);
@ -1620,7 +1620,7 @@ list<name> parser::to_constants(name const & id, char const * msg, pos_info cons
}
if (rs.empty()) {
throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
throw parser_error(sstream() << "unknown identifier '" << id.escape() << "'", p);
}
return to_list(rs);

11
src/util/name.cpp
View file

@ -60,13 +60,20 @@ void name::imp::display_core(std::ostream & out, imp * p, bool escape, char cons
}
if (p->m_is_string) {
size_t sz = strlen(p->m_str);
bool must_escape = escape && *p->m_str && !is_id_first(p->m_str, p->m_str + sz);
bool must_escape = false;
if (escape && *p->m_str) {
if (!is_id_first(p->m_str, p->m_str + sz))
must_escape = true;
// don't escape names produced by server::display_decl
if (must_escape && p->m_str[0] == '?')
must_escape = false;
if (escape) {
for (char * s = p->m_str; !must_escape && *s; s += get_utf8_size(*s)) {
for (char * s = p->m_str + get_utf8_size(p->m_str[0]); !must_escape && *s; s += get_utf8_size(*s)) {
if (!is_id_rest(s, p->m_str + sz))
must_escape = true;
}
}
}
if (must_escape)
out << "«" << p->m_str << "»";
else