Show More
@@ -19,6 +19,7 b' class HistoryConsoleWidget(ConsoleWidget):' | |||||
19 |
|
19 | |||
20 | # HistoryConsoleWidget protected variables. |
|
20 | # HistoryConsoleWidget protected variables. | |
21 | self._history = [] |
|
21 | self._history = [] | |
|
22 | self._history_edits = {} | |||
22 | self._history_index = 0 |
|
23 | self._history_index = 0 | |
23 | self._history_prefix = '' |
|
24 | self._history_prefix = '' | |
24 |
|
25 | |||
@@ -42,6 +43,9 b' class HistoryConsoleWidget(ConsoleWidget):' | |||||
42 | if history and (not self._history or self._history[-1] != history): |
|
43 | if history and (not self._history or self._history[-1] != history): | |
43 | self._history.append(history) |
|
44 | self._history.append(history) | |
44 |
|
45 | |||
|
46 | # Emulate readline: reset all history edits. | |||
|
47 | self._history_edits = {} | |||
|
48 | ||||
45 | # Move the history index to the most recent item. |
|
49 | # Move the history index to the most recent item. | |
46 | self._history_index = len(self._history) |
|
50 | self._history_index = len(self._history) | |
47 |
|
51 | |||
@@ -113,7 +117,7 b' class HistoryConsoleWidget(ConsoleWidget):' | |||||
113 | #--------------------------------------------------------------------------- |
|
117 | #--------------------------------------------------------------------------- | |
114 |
|
118 | |||
115 | def history_previous(self, prefix=''): |
|
119 | def history_previous(self, prefix=''): | |
116 |
""" If possible, set the input buffer to a previous |
|
120 | """ If possible, set the input buffer to a previous history item. | |
117 |
|
121 | |||
118 | Parameters: |
|
122 | Parameters: | |
119 | ----------- |
|
123 | ----------- | |
@@ -123,40 +127,42 b' class HistoryConsoleWidget(ConsoleWidget):' | |||||
123 | index = self._history_index |
|
127 | index = self._history_index | |
124 | while index > 0: |
|
128 | while index > 0: | |
125 | index -= 1 |
|
129 | index -= 1 | |
126 |
history = self._history |
|
130 | history = self._get_edited_history(index) | |
127 | if history.startswith(prefix): |
|
131 | if history.startswith(prefix): | |
128 | break |
|
132 | break | |
129 | else: |
|
133 | else: | |
130 | history = None |
|
134 | history = None | |
131 |
|
135 | |||
132 | if history is not None: |
|
136 | if history is not None: | |
|
137 | self._set_edited_input_buffer(history) | |||
133 | self._history_index = index |
|
138 | self._history_index = index | |
134 | self.input_buffer = history |
|
|||
135 |
|
139 | |||
136 | def history_next(self, prefix=''): |
|
140 | def history_next(self, prefix=''): | |
137 |
""" |
|
141 | """ If possible, set the input buffer to a subsequent history item. | |
138 | original search prefix if there is no such item. |
|
|||
139 |
|
142 | |||
140 | Parameters: |
|
143 | Parameters: | |
141 | ----------- |
|
144 | ----------- | |
142 | prefix : str, optional |
|
145 | prefix : str, optional | |
143 | If specified, search for an item with this prefix. |
|
146 | If specified, search for an item with this prefix. | |
144 | """ |
|
147 | """ | |
145 |
|
|
148 | index = self._history_index | |
146 |
|
|
149 | while self._history_index < len(self._history): | |
147 | history = self._history[self._history_index] |
|
150 | index += 1 | |
|
151 | history = self._get_edited_history(index) | |||
148 | if history.startswith(prefix): |
|
152 | if history.startswith(prefix): | |
149 | break |
|
153 | break | |
150 | else: |
|
154 | else: | |
151 | self._history_index = len(self._history) |
|
155 | history = None | |
152 | history = prefix |
|
156 | ||
153 | self.input_buffer = history |
|
157 | if history is not None: | |
|
158 | self._set_edited_input_buffer(history) | |||
|
159 | self._history_index = index | |||
154 |
|
160 | |||
155 | def history_tail(self, n=10): |
|
161 | def history_tail(self, n=10): | |
156 | """ Get the local history list. |
|
162 | """ Get the local history list. | |
157 |
|
163 | |||
158 | Parameters |
|
164 | Parameters: | |
159 | ---------- |
|
165 | ----------- | |
160 | n : int |
|
166 | n : int | |
161 | The (maximum) number of history items to get. |
|
167 | The (maximum) number of history items to get. | |
162 | """ |
|
168 | """ | |
@@ -166,8 +172,23 b' class HistoryConsoleWidget(ConsoleWidget):' | |||||
166 | # 'HistoryConsoleWidget' protected interface |
|
172 | # 'HistoryConsoleWidget' protected interface | |
167 | #--------------------------------------------------------------------------- |
|
173 | #--------------------------------------------------------------------------- | |
168 |
|
174 | |||
|
175 | def _get_edited_history(self, index): | |||
|
176 | """ Retrieves a history item, possibly with temporary edits. | |||
|
177 | """ | |||
|
178 | if index in self._history_edits: | |||
|
179 | return self._history_edits[index] | |||
|
180 | return self._history[index] | |||
|
181 | ||||
|
182 | def _set_edited_input_buffer(self, source): | |||
|
183 | """ Sets the input buffer to 'source', saving the current input buffer | |||
|
184 | as a temporary history edit. | |||
|
185 | """ | |||
|
186 | self._history_edits[self._history_index] = self.input_buffer | |||
|
187 | self.input_buffer = source | |||
|
188 | ||||
169 | def _set_history(self, history): |
|
189 | def _set_history(self, history): | |
170 | """ Replace the current history with a sequence of history items. |
|
190 | """ Replace the current history with a sequence of history items. | |
171 | """ |
|
191 | """ | |
172 | self._history = list(history) |
|
192 | self._history = list(history) | |
|
193 | self._history_edits = {} | |||
173 | self._history_index = len(self._history) |
|
194 | self._history_index = len(self._history) |
General Comments 0
You need to be logged in to leave comments.
Login now