diff options
| -rw-r--r-- | config/readline.m4 | 11 | ||||
| -rw-r--r-- | configure.ac | 1 | ||||
| -rw-r--r-- | src/main/interactive_shell.cpp | 6 |
3 files changed, 17 insertions, 1 deletions
diff --git a/config/readline.m4 b/config/readline.m4 index 957836285..dcf9a9c18 100644 --- a/config/readline.m4 +++ b/config/readline.m4 @@ -5,6 +5,7 @@ AC_DEFUN([CVC4_CHECK_FOR_READLINE], [ AC_MSG_CHECKING([whether user requested readline support]) LIBREADLINE= have_libreadline=0 +readline_compentry_func_returns_charp=0 READLINE_LIBS= if test "$with_readline" = no; then AC_MSG_RESULT([no, readline disabled by user]) @@ -58,6 +59,16 @@ else fi if test "$with_readline" = yes; then have_libreadline=1 + AC_MSG_CHECKING([for type of rl_completion_entry_function]) + AC_LANG_PUSH([C++]) + AC_COMPILE_IFELSE([AC_LANG_PROGRAM([ +#include <readline/readline.h> +char* foo(const char*, int) { return (char*)0; }],[ +::rl_completion_entry_function = foo;])], + [AC_MSG_RESULT([char* (*)(const char*, int)]) + readline_compentry_func_returns_charp=1], + [AC_MSG_FAILURE([Function])]) + AC_LANG_POP([C++]) else have_libreadline=0 READLINE_LIBS= diff --git a/configure.ac b/configure.ac index 4595227a4..70351681b 100644 --- a/configure.ac +++ b/configure.ac @@ -891,6 +891,7 @@ fi AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check]) CVC4_CHECK_FOR_READLINE AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline]) +AC_DEFINE_UNQUOTED([READLINE_COMPENTRY_FUNC_RETURNS_CHARP], $readline_compentry_func_returns_charp, [Define to 1 if rl_completion_entry_function is declared to return pointer to char]) AC_SUBST([READLINE_LIBS]) AC_SEARCH_LIBS([clock_gettime], [rt], diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index cdeef23ed..7cef623e9 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -94,8 +94,12 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, #if HAVE_LIBREADLINE if(d_in == cin) { - ::rl_readline_name = "CVC4"; + ::rl_readline_name = const_cast<char*>("CVC4"); +#if READLINE_COMPENTRY_FUNC_RETURNS_CHARP ::rl_completion_entry_function = commandGenerator; +#else /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */ + ::rl_completion_entry_function = (Function) commandGenerator; +#endif /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */ ::using_history(); switch(OutputLanguage lang = toOutputLanguage(d_options[options::inputLanguage])) { |