##// END OF EJS Templates
Improve readline resetter mechanism.
Thomas Kluyver -
Show More
@@ -140,17 +140,29 b' class ReadlineNoRecord(object):'
140 140
141 141 def __enter__(self):
142 142 if self._nested_level == 0:
143 self.orig_length = self.current_length()
143 144 self.readline_tail = self.get_readline_tail()
144 145 self._nested_level += 1
145 146
146 147 def __exit__(self, type, value, traceback):
147 148 self._nested_level -= 1
148 149 if self._nested_level == 0:
149 if self.get_readline_tail() != self.readline_tail:
150 # Try clipping the end if it's got longer
151 e = self.current_length() - self.orig_length
152 if e > 0:
153 for _ in range(e):
154 self.shell.readline.remove_history_item(self.orig_length)
155
156 # If it still doesn't match, just reload readline history.
157 if self.current_length() != self.orig_length \
158 or self.get_readline_tail() != self.readline_tail:
150 159 self.shell.refill_readline_hist()
151 160 # Returning False will cause exceptions to propagate
152 161 return False
153
162
163 def current_length(self):
164 return self.shell.readline.get_current_history_length()
165
154 166 def get_readline_tail(self, n=10):
155 167 """Get the last n items in readline history."""
156 168 end = self.shell.readline.get_current_history_length() + 1
General Comments 0
You need to be logged in to leave comments. Login now