fix(frontends/lean/parser): make sure Lean passes all tests when being compiled with the readline library

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser.cpp

@@ -2524,6 +2524,77 @@ io_state parser::get_io_state() const {
     return m_ptr->m_io_state;
 }
 
+#ifdef LEAN_USE_READLINE
+// Hackish wrapper for implementing a streambuf on top of the readline library
+class readline_streambuf : public std::streambuf {
+    std::string      m_buffer;
+    std::streamsize  m_curr;
+    std::streamsize  m_high;
+protected:
+    virtual int_type underflow() {
+        while (m_curr == m_high) {
+            char * line = readline("");
+            if (!line) {
+                // EOF received
+                return traits_type::eof();
+            } else if (strlen(line) == 0) {
+                // ignore blank line
+                m_buffer.push_back('\n');
+                free(line);
+            } else {
+                add_history(line);
+                m_buffer += line;
+                m_buffer.push_back('\n');
+                free(line);
+                m_high = m_buffer.size();
+            }
+        }
+
+        return traits_type::to_int_type(m_buffer[m_curr]);
+    }
+
+    virtual int_type uflow() {
+        int_type r = underflow();
+        if (r != traits_type::eof())
+            m_curr++;
+        return r;
+    }
+
+    virtual int_type pbackfail(int_type c) {
+        if (m_curr == 0)
+            return traits_type::eof();
+        m_curr--;
+        if (c != traits_type::eof())
+            m_buffer[m_curr] = c;
+        return traits_type::eof() + 1; // something different from eof()
+    }
+
+    virtual std::streamsize showmanyc() {
+        return m_high - m_curr;
+    }
+
+public:
+    readline_streambuf():
+        m_curr(0), m_high(0) {
+        setbuf(0, 0);
+    }
+};
+
+struct readline_config {
+    FILE * m_devnull;
+    readline_config() {
+        // By default, the readline library echos the input in the standard output.
+        // We can change this behavior by setting rl_outstream to /dev/null
+        m_devnull = fopen("/dev/null", "a");
+        rl_outstream = m_devnull;
+    }
+    ~readline_config() {
+        fclose(m_devnull);
+    }
+};
+static readline_config g_readline_config;
+#endif
+
 shell::shell(environment const & env, io_state const & ios, script_state * S):m_env(env), m_io_state(ios), m_script_state(S) {
 }
 
@@ -2536,24 +2607,13 @@ shell::~shell() {
 
 bool shell::operator()() {
 #ifdef LEAN_USE_READLINE
-    bool errors = false;
+    readline_streambuf buf;
-    while (true) {
+    std::istream is(&buf);
-        char * input = readline("# ");
+    parser p(m_env, m_io_state, is, m_script_state, false, true);
-        if (!input)
-            return errors;
-        add_history(input);
-        std::istringstream strm(input);
-        {
-            parser p(m_env, m_io_state, strm, m_script_state, false, false);
-            if (!p())
-                errors = true;
-        }
-        free(input);
-    }
 #else
     parser p(m_env, m_io_state, std::cin, m_script_state, false, true);
-    return p();
 #endif
+    return p();
 }
 
 bool parse_commands(environment const & env, io_state & ios, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {