fix(frontends/lean/scanner): do not treat 0xFF as end-of-file

Fixes #1624.  We just replace 0xFF by 0x00 when reading a new input
byte.  This shows up as an unexpected token error.
This commit is contained in:
Gabriel Ebner 2017-05-31 16:54:04 +02:00
parent b59e1b0a2e
commit b1e417805e
4 changed files with 18 additions and 0 deletions

View file

@ -76,6 +76,7 @@ void scanner::fetch_line() {
m_spos = 0;
m_upos = 0;
m_curr = m_curr_line[m_spos];
if (m_curr == EOF) m_curr = 0;
m_uskip = get_utf8_size(m_curr);
m_uskip--;
} else {
@ -96,6 +97,7 @@ void scanner::next() {
}
}
m_curr = m_curr_line[m_spos];
if (m_curr == EOF) m_curr = 0;
if (m_uskip > 0) {
if (!is_utf8_next(m_curr))
throw_exception("invalid utf-8 sequence character");

View file

@ -406,6 +406,9 @@ std::vector<module_name> module_mgr::get_direct_imports(module_id const & id, st
std::istringstream in(contents);
bool use_exceptions = true;
parser p(get_initial_env(), m_ios, nullptr, in, id, use_exceptions);
try {
p.init_scanner();
} catch (...) {}
p.get_imports(imports);
} catch (...) {}

6
tests/lean/ff_byte.lean Normal file
View file

@ -0,0 +1,6 @@
ÿ --<-- should report invalid utf-8 here
def -- TODO(gabriel): let the parser recover
example : false := trivial
-- ^^ and complain about the wrong proof

View file

@ -0,0 +1,7 @@
ff_byte.lean:1:0: error: unexpected token
ff_byte.lean:5:19: error: type mismatch, expression
trivial
has type
true
but is expected to have type
false