From e8df6f67cc2654f50d49995377a4b411668235e1 Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Fri, 17 Jul 2020 18:09:14 +0100 Subject: Support for using 'libedit' over 'readline' #4571 (#4579) Signed-off-by: Andrew V. Jones --- src/main/CMakeLists.txt | 8 ++--- src/main/interactive_shell.cpp | 75 +++++++++++++++++++++++------------------- src/main/interactive_shell.h | 2 +- 3 files changed, 46 insertions(+), 39 deletions(-) (limited to 'src/main') diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 4fbb14183..c168daeaa 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -68,10 +68,10 @@ if(ENABLE_STATIC_BINARY) set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON) endif() -if(USE_READLINE) - target_link_libraries(cvc4-bin ${Readline_LIBRARIES}) - target_link_libraries(main-test ${Readline_LIBRARIES}) - target_include_directories(main PRIVATE ${Readline_INCLUDE_DIR}) +if(USE_EDITLINE) + target_link_libraries(cvc4-bin ${Editline_LIBRARIES}) + target_link_libraries(main-test ${Editline_LIBRARIES}) + target_include_directories(main PRIVATE ${Editline_INCLUDE_DIR}) endif() #-----------------------------------------------------------------------------# diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 17b792ab4..87ebf99cf 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -12,7 +12,7 @@ ** \brief Interactive shell for CVC4 ** ** This file is the implementation for the CVC4 interactive shell. - ** The shell supports the readline library. + ** The shell supports the editline library. **/ #include "main/interactive_shell.h" @@ -26,16 +26,15 @@ #include #include -//This must go before HAVE_LIBREADLINE. +// This must go before HAVE_LIBEDITLINE. #include "cvc4autoconfig.h" -#if HAVE_LIBREADLINE -# include -# include +#if HAVE_LIBEDITLINE +#include # if HAVE_EXT_STDIO_FILEBUF_H # include # endif /* HAVE_EXT_STDIO_FILEBUF_H */ -#endif /* HAVE_LIBREADLINE */ +#endif /* HAVE_LIBEDITLINE */ #include "api/cvc4cpp.h" #include "base/output.h" @@ -56,7 +55,7 @@ using namespace language; const string InteractiveShell::INPUT_FILENAME = ""; -#if HAVE_LIBREADLINE +#if HAVE_LIBEDITLINE #if HAVE_EXT_STDIO_FILEBUF_H using __gnu_cxx::stdio_filebuf; @@ -82,7 +81,7 @@ static const std::string* commandsEnd; static set s_declarations; -#endif /* HAVE_LIBREADLINE */ +#endif /* HAVE_LIBEDITLINE */ InteractiveShell::InteractiveShell(api::Solver* solver) : d_options(solver->getOptions()), @@ -98,14 +97,14 @@ InteractiveShell::InteractiveShell(api::Solver* solver) d_parser->forceLogic(tmp.getLogicString()); } -#if HAVE_LIBREADLINE +#if HAVE_LIBEDITLINE if(&d_in == &cin) { ::rl_readline_name = const_cast("CVC4"); -#if READLINE_COMPENTRY_FUNC_RETURNS_CHARP +#if EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP ::rl_completion_entry_function = commandGenerator; -#else /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */ +#else /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */ ::rl_completion_entry_function = (int (*)(const char*, int)) commandGenerator; -#endif /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */ +#endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */ ::using_history(); OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage()); @@ -135,7 +134,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver) throw Exception(ss.str()); } } - d_usingReadline = true; + d_usingEditline = true; int err = ::read_history(d_historyFilename.c_str()); ::stifle_history(s_historyLimit); if(Notice.isOn()) { @@ -148,15 +147,15 @@ InteractiveShell::InteractiveShell(api::Solver* solver) } } } else { - d_usingReadline = false; + d_usingEditline = false; } -#else /* HAVE_LIBREADLINE */ - d_usingReadline = false; -#endif /* HAVE_LIBREADLINE */ +#else /* HAVE_LIBEDITLINE */ + d_usingEditline = false; +#endif /* HAVE_LIBEDITLINE */ }/* InteractiveShell::InteractiveShell() */ InteractiveShell::~InteractiveShell() { -#if HAVE_LIBREADLINE +#if HAVE_LIBEDITLINE int err = ::write_history(d_historyFilename.c_str()); if(err == 0) { Notice() << "Wrote " << ::history_length << " lines of history to " @@ -165,7 +164,7 @@ InteractiveShell::~InteractiveShell() { Notice() << "Could not write history to " << d_historyFilename << ": " << strerror(err) << std::endl; } -#endif /* HAVE_LIBREADLINE */ +#endif /* HAVE_LIBEDITLINE */ delete d_parser; } @@ -189,8 +188,9 @@ restart: } /* Prompt the user for input. */ - if(d_usingReadline) { -#if HAVE_LIBREADLINE + if (d_usingEditline) + { +#if HAVE_LIBEDITLINE lineBuf = ::readline(d_options.getInteractivePrompt() ? (line == "" ? "CVC4> " : "... > ") : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { @@ -198,8 +198,10 @@ restart: } line += lineBuf == NULL ? "" : lineBuf; free(lineBuf); -#endif /* HAVE_LIBREADLINE */ - } else { +#endif /* HAVE_LIBEDITLINE */ + } + else + { if(d_options.getInteractivePrompt()) { if(line == "") { d_out << "CVC4> " << flush; @@ -236,8 +238,9 @@ restart: } /* If we hit EOF, we're done. */ - if( (!d_usingReadline && d_in.eof()) || - (d_usingReadline && lineBuf == NULL) ) { + if ((!d_usingEditline && d_in.eof()) + || (d_usingEditline && lineBuf == NULL)) + { input += line; if(input.empty()) { @@ -254,7 +257,8 @@ restart: goto restart; } - if(!d_usingReadline) { + if (!d_usingEditline) + { /* Extract the newline delimiter from the stream too */ int c CVC4_UNUSED = d_in.get(); assert(c == '\n'); @@ -268,16 +272,19 @@ restart: n = input.length() - 1; if( !line.empty() && input[n] == '\\' ) { input[n] = '\n'; - if(d_usingReadline) { -#if HAVE_LIBREADLINE + if (d_usingEditline) + { +#if HAVE_LIBEDITLINE lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } line = lineBuf == NULL ? "" : lineBuf; free(lineBuf); -#endif /* HAVE_LIBREADLINE */ - } else { +#endif /* HAVE_LIBEDITLINE */ + } + else + { if(d_options.getInteractivePrompt()) { d_out << "... > " << flush; } @@ -309,7 +316,7 @@ restart: d_quit = true; break; } else { -#if HAVE_LIBREADLINE +#if HAVE_LIBEDITLINE if(dynamic_cast(cmd) != NULL) { s_declarations.insert(dynamic_cast(cmd)->getSymbol()); } else if(dynamic_cast(cmd) != NULL) { @@ -319,7 +326,7 @@ restart: } else if(dynamic_cast(cmd) != NULL) { s_declarations.insert(dynamic_cast(cmd)->getSymbol()); } -#endif /* HAVE_LIBREADLINE */ +#endif /* HAVE_LIBEDITLINE */ } } } catch(ParserEndOfFileException& pe) { @@ -350,7 +357,7 @@ restart: return cmd_seq; }/* InteractiveShell::readCommand() */ -#if HAVE_LIBREADLINE +#if HAVE_LIBEDITLINE char** commandCompletion(const char* text, int start, int end) { Debug("rl") << "text: " << text << endl; @@ -400,6 +407,6 @@ char* commandGenerator(const char* text, int state) { return *rlDeclaration == jj ? NULL : strdup((*(*rlDeclaration)++).c_str()); } -#endif /* HAVE_LIBREADLINE */ +#endif /* HAVE_LIBEDITLINE */ }/* CVC4 namespace */ diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 87845b0ed..f4edb1015 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -42,7 +42,7 @@ class CVC4_PUBLIC InteractiveShell std::ostream& d_out; parser::Parser* d_parser; bool d_quit; - bool d_usingReadline; + bool d_usingEditline; std::string d_historyFilename; -- cgit v1.2.3