From b1e417805eb9bf3d389c9bf8eaa4efeaefc0895f Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 31 May 2017 16:54:04 +0200
Subject: [PATCH] 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.
---
 src/frontends/lean/scanner.cpp       | 2 ++
 src/library/module_mgr.cpp           | 3 +++
 tests/lean/ff_byte.lean              | 6 ++++++
 tests/lean/ff_byte.lean.expected.out | 7 +++++++
 4 files changed, 18 insertions(+)
 create mode 100644 tests/lean/ff_byte.lean
 create mode 100644 tests/lean/ff_byte.lean.expected.out

diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 0994440556..b2594cca54 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -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");
diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp
index 6841264a19..593f53861b 100644
--- a/src/library/module_mgr.cpp
+++ b/src/library/module_mgr.cpp
@@ -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 (...) {}
 
diff --git a/tests/lean/ff_byte.lean b/tests/lean/ff_byte.lean
new file mode 100644
index 0000000000..e1c720b294
--- /dev/null
+++ b/tests/lean/ff_byte.lean
@@ -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
diff --git a/tests/lean/ff_byte.lean.expected.out b/tests/lean/ff_byte.lean.expected.out
new file mode 100644
index 0000000000..e997583119
--- /dev/null
+++ b/tests/lean/ff_byte.lean.expected.out
@@ -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