From e60e20a11d1a3d67df226f7aa06bccb778f6fbce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Dec 2013 10:40:20 -0800 Subject: [PATCH] feat(frontends/lean): add Exit command Remark: on Windows, Ctrl-D does not seem to work. So, this commit also changes the Lean startup message. Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 12 +++++++++--- src/shell/lean.cpp | 6 +++++- tests/lean/exit.lean | 2 ++ tests/lean/exit.lean.expected.out | 2 ++ 4 files changed, 18 insertions(+), 4 deletions(-) create mode 100644 tests/lean/exit.lean create mode 100644 tests/lean/exit.lean.expected.out diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index a0a87637b0..6205d93557 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -92,12 +92,13 @@ static name g_env_kwd("Environment"); static name g_import_kwd("Import"); static name g_help_kwd("Help"); static name g_coercion_kwd("Coercion"); +static name g_exit_kwd("Exit"); static name g_apply("apply"); static name g_done("done"); /** \brief Table/List with all builtin command keywords */ static list g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd, g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd, - g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd}; + g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd, g_exit_kwd}; // ========================================== // ========================================== @@ -1592,6 +1593,7 @@ class parser::imp { << " Theorem [id] : [type] := [expr] define a new theorem" << endl << " Echo [string] display the given string" << endl << " Eval [expr] evaluate the given expression" << endl + << " Exit exit" << endl << " Help display this message" << endl << " Help Options display available options" << endl << " Help Notation describe commands for defining infix, mixfix, postfix operators" << endl @@ -1617,7 +1619,7 @@ class parser::imp { } /** \brief Parse a Lean command. */ - void parse_command() { + bool parse_command() { m_elaborator.clear(); m_expr_pos_info.clear(); m_last_cmd_pos = pos(); @@ -1656,10 +1658,14 @@ class parser::imp { parse_help(); } else if (cmd_id == g_coercion_kwd) { parse_coercion(); + } else if (cmd_id == g_exit_kwd) { + next(); + return false; } else { next(); throw parser_error(sstream() << "invalid command '" << cmd_id << "'", m_last_cmd_pos); } + return true; } /*@}*/ @@ -1798,7 +1804,7 @@ public: while (true) { try { switch (curr()) { - case scanner::token::CommandId: parse_command(); break; + case scanner::token::CommandId: if (!parse_command()) return !m_found_errors; break; case scanner::token::ScriptBlock: parse_script(); break; case scanner::token::Period: show_prompt(); next(); break; case scanner::token::Eof: return !m_found_errors; diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index d98ea6534a..73b0132404 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -108,7 +108,11 @@ int main(int argc, char ** argv) { script_state S; if (optind >= argc) { display_header(std::cout); - std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl; + #if defined(LEAN_WINDOWS) + std::cout << "Type 'Exit.' to exit or 'Help.' for help."<< std::endl; + #else + std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl; + #endif shell sh(f, &S); signal(SIGINT, on_ctrl_c); return sh(); diff --git a/tests/lean/exit.lean b/tests/lean/exit.lean new file mode 100644 index 0000000000..bf6df28db6 --- /dev/null +++ b/tests/lean/exit.lean @@ -0,0 +1,2 @@ +Exit +Show "FAILED" diff --git a/tests/lean/exit.lean.expected.out b/tests/lean/exit.lean.expected.out new file mode 100644 index 0000000000..1a86da9631 --- /dev/null +++ b/tests/lean/exit.lean.expected.out @@ -0,0 +1,2 @@ + Set: pp::colors + Set: pp::unicode