Show More
@@ -1,173 +1,194 b'' | |||||
1 | # System library imports |
|
1 | # System library imports | |
2 | from IPython.external.qt import QtGui |
|
2 | from IPython.external.qt import QtGui | |
3 |
|
3 | |||
4 | # Local imports |
|
4 | # Local imports | |
5 | from console_widget import ConsoleWidget |
|
5 | from console_widget import ConsoleWidget | |
6 |
|
6 | |||
7 |
|
7 | |||
8 | class HistoryConsoleWidget(ConsoleWidget): |
|
8 | class HistoryConsoleWidget(ConsoleWidget): | |
9 | """ A ConsoleWidget that keeps a history of the commands that have been |
|
9 | """ A ConsoleWidget that keeps a history of the commands that have been | |
10 | executed and provides a readline-esque interface to this history. |
|
10 | executed and provides a readline-esque interface to this history. | |
11 | """ |
|
11 | """ | |
12 |
|
12 | |||
13 | #--------------------------------------------------------------------------- |
|
13 | #--------------------------------------------------------------------------- | |
14 | # 'object' interface |
|
14 | # 'object' interface | |
15 | #--------------------------------------------------------------------------- |
|
15 | #--------------------------------------------------------------------------- | |
16 |
|
16 | |||
17 | def __init__(self, *args, **kw): |
|
17 | def __init__(self, *args, **kw): | |
18 | super(HistoryConsoleWidget, self).__init__(*args, **kw) |
|
18 | super(HistoryConsoleWidget, self).__init__(*args, **kw) | |
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 | |||
25 | #--------------------------------------------------------------------------- |
|
26 | #--------------------------------------------------------------------------- | |
26 | # 'ConsoleWidget' public interface |
|
27 | # 'ConsoleWidget' public interface | |
27 | #--------------------------------------------------------------------------- |
|
28 | #--------------------------------------------------------------------------- | |
28 |
|
29 | |||
29 | def execute(self, source=None, hidden=False, interactive=False): |
|
30 | def execute(self, source=None, hidden=False, interactive=False): | |
30 | """ Reimplemented to the store history. |
|
31 | """ Reimplemented to the store history. | |
31 | """ |
|
32 | """ | |
32 | if not hidden: |
|
33 | if not hidden: | |
33 | history = self.input_buffer if source is None else source |
|
34 | history = self.input_buffer if source is None else source | |
34 |
|
35 | |||
35 | executed = super(HistoryConsoleWidget, self).execute( |
|
36 | executed = super(HistoryConsoleWidget, self).execute( | |
36 | source, hidden, interactive) |
|
37 | source, hidden, interactive) | |
37 |
|
38 | |||
38 | if executed and not hidden: |
|
39 | if executed and not hidden: | |
39 | # Save the command unless it was an empty string or was identical |
|
40 | # Save the command unless it was an empty string or was identical | |
40 | # to the previous command. |
|
41 | # to the previous command. | |
41 | history = history.rstrip() |
|
42 | history = history.rstrip() | |
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 | |||
48 | return executed |
|
52 | return executed | |
49 |
|
53 | |||
50 | #--------------------------------------------------------------------------- |
|
54 | #--------------------------------------------------------------------------- | |
51 | # 'ConsoleWidget' abstract interface |
|
55 | # 'ConsoleWidget' abstract interface | |
52 | #--------------------------------------------------------------------------- |
|
56 | #--------------------------------------------------------------------------- | |
53 |
|
57 | |||
54 | def _up_pressed(self): |
|
58 | def _up_pressed(self): | |
55 | """ Called when the up key is pressed. Returns whether to continue |
|
59 | """ Called when the up key is pressed. Returns whether to continue | |
56 | processing the event. |
|
60 | processing the event. | |
57 | """ |
|
61 | """ | |
58 | prompt_cursor = self._get_prompt_cursor() |
|
62 | prompt_cursor = self._get_prompt_cursor() | |
59 | if self._get_cursor().blockNumber() == prompt_cursor.blockNumber(): |
|
63 | if self._get_cursor().blockNumber() == prompt_cursor.blockNumber(): | |
60 |
|
64 | |||
61 | # Set a search prefix based on the cursor position. |
|
65 | # Set a search prefix based on the cursor position. | |
62 | col = self._get_input_buffer_cursor_column() |
|
66 | col = self._get_input_buffer_cursor_column() | |
63 | input_buffer = self.input_buffer |
|
67 | input_buffer = self.input_buffer | |
64 | if self._history_index == len(self._history) or \ |
|
68 | if self._history_index == len(self._history) or \ | |
65 | (self._history_prefix and col != len(self._history_prefix)): |
|
69 | (self._history_prefix and col != len(self._history_prefix)): | |
66 | self._history_index = len(self._history) |
|
70 | self._history_index = len(self._history) | |
67 | self._history_prefix = input_buffer[:col] |
|
71 | self._history_prefix = input_buffer[:col] | |
68 |
|
72 | |||
69 | # Perform the search. |
|
73 | # Perform the search. | |
70 | self.history_previous(self._history_prefix) |
|
74 | self.history_previous(self._history_prefix) | |
71 |
|
75 | |||
72 | # Go to the first line of the prompt for seemless history scrolling. |
|
76 | # Go to the first line of the prompt for seemless history scrolling. | |
73 | # Emulate readline: keep the cursor position fixed for a prefix |
|
77 | # Emulate readline: keep the cursor position fixed for a prefix | |
74 | # search. |
|
78 | # search. | |
75 | cursor = self._get_prompt_cursor() |
|
79 | cursor = self._get_prompt_cursor() | |
76 | if self._history_prefix: |
|
80 | if self._history_prefix: | |
77 | cursor.movePosition(QtGui.QTextCursor.Right, |
|
81 | cursor.movePosition(QtGui.QTextCursor.Right, | |
78 | n=len(self._history_prefix)) |
|
82 | n=len(self._history_prefix)) | |
79 | else: |
|
83 | else: | |
80 | cursor.movePosition(QtGui.QTextCursor.EndOfLine) |
|
84 | cursor.movePosition(QtGui.QTextCursor.EndOfLine) | |
81 | self._set_cursor(cursor) |
|
85 | self._set_cursor(cursor) | |
82 |
|
86 | |||
83 | return False |
|
87 | return False | |
84 |
|
88 | |||
85 | return True |
|
89 | return True | |
86 |
|
90 | |||
87 | def _down_pressed(self): |
|
91 | def _down_pressed(self): | |
88 | """ Called when the down key is pressed. Returns whether to continue |
|
92 | """ Called when the down key is pressed. Returns whether to continue | |
89 | processing the event. |
|
93 | processing the event. | |
90 | """ |
|
94 | """ | |
91 | end_cursor = self._get_end_cursor() |
|
95 | end_cursor = self._get_end_cursor() | |
92 | if self._get_cursor().blockNumber() == end_cursor.blockNumber(): |
|
96 | if self._get_cursor().blockNumber() == end_cursor.blockNumber(): | |
93 |
|
97 | |||
94 | # Perform the search. |
|
98 | # Perform the search. | |
95 | self.history_next(self._history_prefix) |
|
99 | self.history_next(self._history_prefix) | |
96 |
|
100 | |||
97 | # Emulate readline: keep the cursor position fixed for a prefix |
|
101 | # Emulate readline: keep the cursor position fixed for a prefix | |
98 | # search. (We don't need to move the cursor to the end of the buffer |
|
102 | # search. (We don't need to move the cursor to the end of the buffer | |
99 | # in the other case because this happens automatically when the |
|
103 | # in the other case because this happens automatically when the | |
100 | # input buffer is set.) |
|
104 | # input buffer is set.) | |
101 | if self._history_prefix: |
|
105 | if self._history_prefix: | |
102 | cursor = self._get_prompt_cursor() |
|
106 | cursor = self._get_prompt_cursor() | |
103 | cursor.movePosition(QtGui.QTextCursor.Right, |
|
107 | cursor.movePosition(QtGui.QTextCursor.Right, | |
104 | n=len(self._history_prefix)) |
|
108 | n=len(self._history_prefix)) | |
105 | self._set_cursor(cursor) |
|
109 | self._set_cursor(cursor) | |
106 |
|
110 | |||
107 | return False |
|
111 | return False | |
108 |
|
112 | |||
109 | return True |
|
113 | return True | |
110 |
|
114 | |||
111 | #--------------------------------------------------------------------------- |
|
115 | #--------------------------------------------------------------------------- | |
112 | # 'HistoryConsoleWidget' public interface |
|
116 | # 'HistoryConsoleWidget' public interface | |
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 | ----------- | |
120 | prefix : str, optional |
|
124 | prefix : str, optional | |
121 | If specified, search for an item with this prefix. |
|
125 | If specified, search for an item with this prefix. | |
122 | """ |
|
126 | """ | |
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 | """ | |
163 | return self._history[-n:] |
|
169 | return self._history[-n:] | |
164 |
|
170 | |||
165 | #--------------------------------------------------------------------------- |
|
171 | #--------------------------------------------------------------------------- | |
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