From 59e63c04219db917620b700f773730910e76f864 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 21 Aug 2013 18:24:26 -0700
Subject: [PATCH] Add prompt when in interactive mode. Fix Show Environment
 [num]

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/exprlib/state.h                |  2 ++
 src/frontends/lean/lean_parser.cpp | 33 ++++++++++++++++++++++--------
 src/frontends/lean/lean_parser.h   |  2 +-
 src/shell/lean.cpp                 |  3 +--
 4 files changed, 29 insertions(+), 11 deletions(-)

diff --git a/src/exprlib/state.h b/src/exprlib/state.h
index 407d3c6a9..db38d0953 100644
--- a/src/exprlib/state.h
+++ b/src/exprlib/state.h
@@ -44,11 +44,13 @@ public:
 struct regular {
     state const & m_state;
     regular(state const & s):m_state(s) {}
+    void flush() { m_state.get_regular_channel().get_stream().flush(); }
 };
 
 struct diagnostic {
     state const & m_state;
     diagnostic(state const & s):m_state(s) {}
+    void flush() { m_state.get_diagnostic_channel().get_stream().flush(); }
 };
 
 // hack for using std::endl with channels
diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp
index f476e8035..0d509b719 100644
--- a/src/frontends/lean/lean_parser.cpp
+++ b/src/frontends/lean/lean_parser.cpp
@@ -89,6 +89,7 @@ class parser_fn {
     scanner        m_scanner;
     scanner::token m_curr;
     bool           m_use_exceptions;
+    bool           m_interactive;
     bool           m_found_errors;
     local_decls    m_local_decls;
     unsigned       m_num_local_decls;
@@ -873,11 +874,14 @@ class parser_fn {
             if (opt_id == g_env_kwd) {
                 if (curr_is_int()) {
                     unsigned i = parse_unsigned("invalid argument, value does not fit in a machine integer");
-                    auto it  = m_frontend.end_objects();
+                    auto end = m_frontend.end_objects();
                     auto beg = m_frontend.begin_objects();
+                    auto it  = end;
                     while (it != beg && i != 0) {
                         --i;
                         --it;
+                    }
+                    for (; it != end; ++it) {
                         regular(m_frontend) << *it << endl;
                     }
                 } else {
@@ -1016,7 +1020,7 @@ class parser_fn {
         std::ifstream in(fname);
         if (!in.is_open())
             throw parser_error("invalid import command, failed to open file");
-        ::lean::parse_commands(m_frontend, in, m_use_exceptions);
+        ::lean::parse_commands(m_frontend, in, m_use_exceptions, false);
     }
 
     void parse_help() {
@@ -1092,10 +1096,11 @@ class parser_fn {
     }
 
 public:
-    parser_fn(frontend & fe, std::istream & in, bool use_exceptions):
+    parser_fn(frontend & fe, std::istream & in, bool use_exceptions, bool interactive):
         m_frontend(fe),
         m_scanner(in),
-        m_use_exceptions(use_exceptions) {
+        m_use_exceptions(use_exceptions),
+        m_interactive(interactive) {
         m_found_errors = false;
         m_num_local_decls = 0;
         m_scanner.set_command_keywords(g_command_keywords);
@@ -1103,13 +1108,24 @@ public:
         scan();
     }
 
+    static void show_prompt(bool interactive, frontend const & fe) {
+        if (interactive) {
+            regular(fe) << "# ";
+            regular(fe).flush();
+        }
+    }
+
+    void show_prompt() {
+        show_prompt(m_interactive, m_frontend);
+    }
+
     /** \brief Parse a sequence of commands. This method also perform error management. */
     bool parse_commands() {
         while (true) {
             try {
                 switch (curr()) {
                 case scanner::token::CommandId: parse_command(); break;
-                case scanner::token::Period: next(); break;
+                case scanner::token::Period: show_prompt(); next(); break;
                 case scanner::token::Eof: return !m_found_errors;
                 default:
                     throw parser_error("Command expected");
@@ -1142,10 +1158,11 @@ public:
     }
 
 };
-bool parse_commands(frontend & fe, std::istream & in, bool use_exceptions) {
-    return parser_fn(fe, in, use_exceptions).parse_commands();
+bool parse_commands(frontend & fe, std::istream & in, bool use_exceptions, bool interactive) {
+    parser_fn::show_prompt(interactive, fe);
+    return parser_fn(fe, in, use_exceptions, interactive).parse_commands();
 }
 expr parse_expr(frontend const & fe, std::istream & in) {
-    return parser_fn(const_cast<frontend&>(fe), in, true).parse_expr_main();
+    return parser_fn(const_cast<frontend&>(fe), in, true, false).parse_expr_main();
 }
 }
diff --git a/src/frontends/lean/lean_parser.h b/src/frontends/lean/lean_parser.h
index a2e07200a..a22dec3c0 100644
--- a/src/frontends/lean/lean_parser.h
+++ b/src/frontends/lean/lean_parser.h
@@ -9,6 +9,6 @@ Author: Leonardo de Moura
 #include "lean_frontend.h"
 
 namespace lean {
-bool parse_commands(frontend & fe, std::istream & in, bool use_exceptions = false);
+bool parse_commands(frontend & fe, std::istream & in, bool use_exceptions = true, bool interactive = false);
 expr parse_expr(frontend const & fe, std::istream & in);
 }
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index aaa05c8c8..c845a2545 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -5,13 +5,12 @@
 #include "lean_parser.h"
 using namespace lean;
 
-
 int main(int argc, char ** argv) {
     std::cout << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ")\n";
     std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl;
     frontend f;
     if (argc == 1) {
-        return parse_commands(f, std::cin) ? 0 : 1;
+        return parse_commands(f, std::cin, false, true) ? 0 : 1;
     } else {
         bool ok = true;
         for (int i = 1; i < argc; i++) {