Index: /trunk/FACT++/src/Readline.cc
===================================================================
--- /trunk/FACT++/src/Readline.cc	(revision 10342)
+++ /trunk/FACT++/src/Readline.cc	(revision 10343)
@@ -155,34 +155,8 @@
 // --------------------------------------------------------------------------
 //
-//! This is a static helper to remove leading and trailing whitespaces.
-//!
-//! @param buf
-//!    a pointer to the char array from which the whitespaces should be
-//!    removed
-//!
-//! @returns
-//!    a std::string with the whitespaces removed from buf
-//
-string Readline::TrimSpaces(const char *buf)
-{
-    const string str(buf);
-
-    // Trim Both leading and trailing spaces
-    const size_t start = str.find_first_not_of(' '); // Find the first character position after excluding leading blank spaces
-    const size_t end   = str.find_last_not_of(' ');  // Find the first character position from reverse af
-
-    // if all spaces or empty return an empty string
-    if (string::npos==start || string::npos==end)
-        return string();
-
-    return str.substr(start, end-start+1);
-}
-
-// --------------------------------------------------------------------------
-//
 //! This wraps the given readline function such that the output can be
 //! redirected from thr rl_outstream to the given C++ ostream.
 //!
-//! @param ostream
+//! @param out
 //!    The stream to which the output should be redirected.
 //!
@@ -537,11 +511,16 @@
         return;
 
+    int p = -1;
     while (skip==2)
     {
-        int p = history_search_pos(str.c_str(), 0, 0);
+        p = history_search_pos(str.c_str(), 0, p+1);
         if (p<0)
             break;
 
-        delete remove_history(p);
+        // It seems like history_search_pos works more like
+        // history_search_prefix, therefore the identity is checked again
+        const HIST_ENTRY *e = history_get(p+1);
+        if (e && str==e->line)
+            delete remove_history(p);
     }
 
@@ -943,4 +922,5 @@
     fprintf(rl_outstream, "   Ctrl-left       One word backward\n");
     fprintf(rl_outstream, "   Ctrl-right      One word forward\n");
+    fprintf(rl_outstream, "   Ctrl-d          Quit\n");
     fprintf(rl_outstream, "   Ctrl-y          Delete line\n");
     fprintf(rl_outstream, "   Alt-end/Ctrl-k  Delete until the end of the line\n");
@@ -1016,5 +996,5 @@
         return false;
 
-    str = TrimSpaces(buf);
+    str = Trim(buf);
 
     free(buf);
@@ -1044,5 +1024,5 @@
     Shutdown(buf ? buf : "");
 
-    const string str = !buf || (rl_done && rl_pending_input) ? ".q" : TrimSpaces(buf);
+    const string str = !buf || (rl_done && rl_pending_input==4) ? ".q" : Trim(buf);
 
     free(buf);
@@ -1100,4 +1080,4 @@
 {
     rl_done          = 1;
-    rl_pending_input = 1;
-}
+    rl_pending_input = 4; // EOT (end of transmission, ctrl-d)
+}
Index: /trunk/FACT++/src/Readline.h
===================================================================
--- /trunk/FACT++/src/Readline.h	(revision 10342)
+++ /trunk/FACT++/src/Readline.h	(revision 10343)
@@ -8,5 +8,4 @@
 {
 public:
-    static std::string TrimSpaces(const char *buf);
     static bool RedirectionWrapper(std::ostream &out, bool (*function)());