Show More
@@ -18,18 +18,19 b' class BracketMatcher(QtCore.QObject):' | |||||
18 | # 'QObject' interface |
|
18 | # 'QObject' interface | |
19 | #-------------------------------------------------------------------------- |
|
19 | #-------------------------------------------------------------------------- | |
20 |
|
20 | |||
21 |
def __init__(self, |
|
21 | def __init__(self, text_edit): | |
22 | """ Create a call tip manager that is attached to the specified Qt |
|
22 | """ Create a call tip manager that is attached to the specified Qt | |
23 | text edit widget. |
|
23 | text edit widget. | |
24 | """ |
|
24 | """ | |
25 |
assert isinstance( |
|
25 | assert isinstance(text_edit, (QtGui.QTextEdit, QtGui.QPlainTextEdit)) | |
26 | QtCore.QObject.__init__(self, parent) |
|
26 | super(BracketMatcher, self).__init__() | |
27 |
|
27 | |||
28 | # The format to apply to matching brackets. |
|
28 | # The format to apply to matching brackets. | |
29 | self.format = QtGui.QTextCharFormat() |
|
29 | self.format = QtGui.QTextCharFormat() | |
30 | self.format.setBackground(QtGui.QColor('silver')) |
|
30 | self.format.setBackground(QtGui.QColor('silver')) | |
31 |
|
31 | |||
32 | parent.cursorPositionChanged.connect(self._cursor_position_changed) |
|
32 | self._text_edit = text_edit | |
|
33 | text_edit.cursorPositionChanged.connect(self._cursor_position_changed) | |||
33 |
|
34 | |||
34 | #-------------------------------------------------------------------------- |
|
35 | #-------------------------------------------------------------------------- | |
35 | # Protected interface |
|
36 | # Protected interface | |
@@ -40,7 +41,7 b' class BracketMatcher(QtCore.QObject):' | |||||
40 | position of the matching bracket. Returns -1 if unsuccessful. |
|
41 | position of the matching bracket. Returns -1 if unsuccessful. | |
41 | """ |
|
42 | """ | |
42 | # Decide what character to search for and what direction to search in. |
|
43 | # Decide what character to search for and what direction to search in. | |
43 |
document = self. |
|
44 | document = self._text_edit.document() | |
44 | qchar = document.characterAt(position) |
|
45 | qchar = document.characterAt(position) | |
45 | start_char = qchar.toAscii() |
|
46 | start_char = qchar.toAscii() | |
46 | search_char = self._opening_map.get(start_char) |
|
47 | search_char = self._opening_map.get(start_char) | |
@@ -73,7 +74,7 b' class BracketMatcher(QtCore.QObject):' | |||||
73 | """ Convenience method for selecting a character. |
|
74 | """ Convenience method for selecting a character. | |
74 | """ |
|
75 | """ | |
75 | selection = QtGui.QTextEdit.ExtraSelection() |
|
76 | selection = QtGui.QTextEdit.ExtraSelection() | |
76 |
cursor = self. |
|
77 | cursor = self._text_edit.textCursor() | |
77 | cursor.setPosition(position) |
|
78 | cursor.setPosition(position) | |
78 | cursor.movePosition(QtGui.QTextCursor.NextCharacter, |
|
79 | cursor.movePosition(QtGui.QTextCursor.NextCharacter, | |
79 | QtGui.QTextCursor.KeepAnchor) |
|
80 | QtGui.QTextCursor.KeepAnchor) | |
@@ -87,15 +88,14 b' class BracketMatcher(QtCore.QObject):' | |||||
87 | """ Updates the document formatting based on the new cursor position. |
|
88 | """ Updates the document formatting based on the new cursor position. | |
88 | """ |
|
89 | """ | |
89 | # Clear out the old formatting. |
|
90 | # Clear out the old formatting. | |
90 |
|
|
91 | self._text_edit.setExtraSelections([]) | |
91 | text_edit.setExtraSelections([]) |
|
|||
92 |
|
92 | |||
93 | # Attempt to match a bracket for the new cursor position. |
|
93 | # Attempt to match a bracket for the new cursor position. | |
94 | cursor = text_edit.textCursor() |
|
94 | cursor = self._text_edit.textCursor() | |
95 | if not cursor.hasSelection(): |
|
95 | if not cursor.hasSelection(): | |
96 | position = cursor.position() - 1 |
|
96 | position = cursor.position() - 1 | |
97 | match_position = self._find_match(position) |
|
97 | match_position = self._find_match(position) | |
98 | if match_position != -1: |
|
98 | if match_position != -1: | |
99 | extra_selections = [ self._selection_for_character(pos) |
|
99 | extra_selections = [ self._selection_for_character(pos) | |
100 | for pos in (position, match_position) ] |
|
100 | for pos in (position, match_position) ] | |
101 | text_edit.setExtraSelections(extra_selections) |
|
101 | self._text_edit.setExtraSelections(extra_selections) |
@@ -14,16 +14,17 b' class CallTipWidget(QtGui.QLabel):' | |||||
14 | # 'QObject' interface |
|
14 | # 'QObject' interface | |
15 | #-------------------------------------------------------------------------- |
|
15 | #-------------------------------------------------------------------------- | |
16 |
|
16 | |||
17 |
def __init__(self, |
|
17 | def __init__(self, text_edit): | |
18 | """ Create a call tip manager that is attached to the specified Qt |
|
18 | """ Create a call tip manager that is attached to the specified Qt | |
19 | text edit widget. |
|
19 | text edit widget. | |
20 | """ |
|
20 | """ | |
21 |
assert isinstance( |
|
21 | assert isinstance(text_edit, (QtGui.QTextEdit, QtGui.QPlainTextEdit)) | |
22 |
|
|
22 | super(CallTipWidget, self).__init__(None, QtCore.Qt.ToolTip) | |
23 |
|
23 | |||
24 | self._hide_timer = QtCore.QBasicTimer() |
|
24 | self._hide_timer = QtCore.QBasicTimer() | |
|
25 | self._text_edit = text_edit | |||
25 |
|
26 | |||
26 |
self.setFont( |
|
27 | self.setFont(text_edit.document().defaultFont()) | |
27 | self.setForegroundRole(QtGui.QPalette.ToolTipText) |
|
28 | self.setForegroundRole(QtGui.QPalette.ToolTipText) | |
28 | self.setBackgroundRole(QtGui.QPalette.ToolTipBase) |
|
29 | self.setBackgroundRole(QtGui.QPalette.ToolTipBase) | |
29 | self.setPalette(QtGui.QToolTip.palette()) |
|
30 | self.setPalette(QtGui.QToolTip.palette()) | |
@@ -37,10 +38,10 b' class CallTipWidget(QtGui.QLabel):' | |||||
37 | QtGui.QStyle.SH_ToolTipLabel_Opacity, None, self) / 255.0) |
|
38 | QtGui.QStyle.SH_ToolTipLabel_Opacity, None, self) / 255.0) | |
38 |
|
39 | |||
39 | def eventFilter(self, obj, event): |
|
40 | def eventFilter(self, obj, event): | |
40 |
""" Reimplemented to hide on certain key presses and on |
|
41 | """ Reimplemented to hide on certain key presses and on text edit focus | |
41 | changes. |
|
42 | changes. | |
42 | """ |
|
43 | """ | |
43 |
if obj == self. |
|
44 | if obj == self._text_edit: | |
44 | etype = event.type() |
|
45 | etype = event.type() | |
45 |
|
46 | |||
46 | if etype == QtCore.QEvent.KeyPress: |
|
47 | if etype == QtCore.QEvent.KeyPress: | |
@@ -60,7 +61,7 b' class CallTipWidget(QtGui.QLabel):' | |||||
60 | elif etype == QtCore.QEvent.Leave: |
|
61 | elif etype == QtCore.QEvent.Leave: | |
61 | self._hide_later() |
|
62 | self._hide_later() | |
62 |
|
63 | |||
63 |
return |
|
64 | return super(CallTipWidget, self).eventFilter(obj, event) | |
64 |
|
65 | |||
65 | def timerEvent(self, event): |
|
66 | def timerEvent(self, event): | |
66 | """ Reimplemented to hide the widget when the hide timer fires. |
|
67 | """ Reimplemented to hide the widget when the hide timer fires. | |
@@ -76,21 +77,21 b' class CallTipWidget(QtGui.QLabel):' | |||||
76 | def enterEvent(self, event): |
|
77 | def enterEvent(self, event): | |
77 | """ Reimplemented to cancel the hide timer. |
|
78 | """ Reimplemented to cancel the hide timer. | |
78 | """ |
|
79 | """ | |
79 |
|
|
80 | super(CallTipWidget, self).enterEvent(event) | |
80 | self._hide_timer.stop() |
|
81 | self._hide_timer.stop() | |
81 |
|
82 | |||
82 | def hideEvent(self, event): |
|
83 | def hideEvent(self, event): | |
83 | """ Reimplemented to disconnect signal handlers and event filter. |
|
84 | """ Reimplemented to disconnect signal handlers and event filter. | |
84 | """ |
|
85 | """ | |
85 | QtGui.QLabel.hideEvent(self, event) |
|
86 | super(CallTipWidget, self).hideEvent(event) | |
86 | parent = self.parent() |
|
87 | self._text_edit.cursorPositionChanged.disconnect( | |
87 |
|
|
88 | self._cursor_position_changed) | |
88 |
|
|
89 | self._text_edit.removeEventFilter(self) | |
89 |
|
90 | |||
90 | def leaveEvent(self, event): |
|
91 | def leaveEvent(self, event): | |
91 | """ Reimplemented to start the hide timer. |
|
92 | """ Reimplemented to start the hide timer. | |
92 | """ |
|
93 | """ | |
93 |
|
|
94 | super(CallTipWidget, self).leaveEvent(event) | |
94 | self._hide_later() |
|
95 | self._hide_later() | |
95 |
|
96 | |||
96 | def paintEvent(self, event): |
|
97 | def paintEvent(self, event): | |
@@ -102,15 +103,15 b' class CallTipWidget(QtGui.QLabel):' | |||||
102 | painter.drawPrimitive(QtGui.QStyle.PE_PanelTipLabel, option) |
|
103 | painter.drawPrimitive(QtGui.QStyle.PE_PanelTipLabel, option) | |
103 | painter.end() |
|
104 | painter.end() | |
104 |
|
105 | |||
105 |
|
|
106 | super(CallTipWidget, self).paintEvent(event) | |
106 |
|
107 | |||
107 | def showEvent(self, event): |
|
108 | def showEvent(self, event): | |
108 | """ Reimplemented to connect signal handlers and event filter. |
|
109 | """ Reimplemented to connect signal handlers and event filter. | |
109 | """ |
|
110 | """ | |
110 | QtGui.QLabel.showEvent(self, event) |
|
111 | super(CallTipWidget, self).showEvent(event) | |
111 | parent = self.parent() |
|
112 | self._text_edit.cursorPositionChanged.connect( | |
112 |
|
|
113 | self._cursor_position_changed) | |
113 |
|
|
114 | self._text_edit.installEventFilter(self) | |
114 |
|
115 | |||
115 | #-------------------------------------------------------------------------- |
|
116 | #-------------------------------------------------------------------------- | |
116 | # 'CallTipWidget' interface |
|
117 | # 'CallTipWidget' interface | |
@@ -131,7 +132,7 b' class CallTipWidget(QtGui.QLabel):' | |||||
131 | """ Attempts to show the specified tip at the current cursor location. |
|
132 | """ Attempts to show the specified tip at the current cursor location. | |
132 | """ |
|
133 | """ | |
133 | # Attempt to find the cursor position at which to show the call tip. |
|
134 | # Attempt to find the cursor position at which to show the call tip. | |
134 |
text_edit = self. |
|
135 | text_edit = self._text_edit | |
135 | document = text_edit.document() |
|
136 | document = text_edit.document() | |
136 | cursor = text_edit.textCursor() |
|
137 | cursor = text_edit.textCursor() | |
137 | search_pos = cursor.position() - 1 |
|
138 | search_pos = cursor.position() - 1 | |
@@ -172,7 +173,7 b' class CallTipWidget(QtGui.QLabel):' | |||||
172 | not found) and the number commas (at depth 0) found along the way. |
|
173 | not found) and the number commas (at depth 0) found along the way. | |
173 | """ |
|
174 | """ | |
174 | commas = depth = 0 |
|
175 | commas = depth = 0 | |
175 |
document = self. |
|
176 | document = self._text_edit.document() | |
176 | qchar = document.characterAt(position) |
|
177 | qchar = document.characterAt(position) | |
177 | while (position > 0 and qchar.isPrint() and |
|
178 | while (position > 0 and qchar.isPrint() and | |
178 | # Need to check explicitly for line/paragraph separators: |
|
179 | # Need to check explicitly for line/paragraph separators: | |
@@ -205,7 +206,7 b' class CallTipWidget(QtGui.QLabel):' | |||||
205 | def _cursor_position_changed(self): |
|
206 | def _cursor_position_changed(self): | |
206 | """ Updates the tip based on user cursor movement. |
|
207 | """ Updates the tip based on user cursor movement. | |
207 | """ |
|
208 | """ | |
208 |
cursor = self. |
|
209 | cursor = self._text_edit.textCursor() | |
209 | if cursor.position() <= self._start_position: |
|
210 | if cursor.position() <= self._start_position: | |
210 | self.hide() |
|
211 | self.hide() | |
211 | else: |
|
212 | else: |
@@ -10,18 +10,20 b' class CompletionWidget(QtGui.QListWidget):' | |||||
10 | # 'QObject' interface |
|
10 | # 'QObject' interface | |
11 | #-------------------------------------------------------------------------- |
|
11 | #-------------------------------------------------------------------------- | |
12 |
|
12 | |||
13 |
def __init__(self, |
|
13 | def __init__(self, text_edit): | |
14 | """ Create a completion widget that is attached to the specified Qt |
|
14 | """ Create a completion widget that is attached to the specified Qt | |
15 | text edit widget. |
|
15 | text edit widget. | |
16 | """ |
|
16 | """ | |
17 |
assert isinstance( |
|
17 | assert isinstance(text_edit, (QtGui.QTextEdit, QtGui.QPlainTextEdit)) | |
18 | QtGui.QListWidget.__init__(self, parent) |
|
18 | super(CompletionWidget, self).__init__() | |
|
19 | ||||
|
20 | self._text_edit = text_edit | |||
19 |
|
21 | |||
20 | self.setWindowFlags(QtCore.Qt.ToolTip | QtCore.Qt.WindowStaysOnTopHint) |
|
|||
21 | self.setAttribute(QtCore.Qt.WA_StaticContents) |
|
22 | self.setAttribute(QtCore.Qt.WA_StaticContents) | |
|
23 | self.setWindowFlags(QtCore.Qt.ToolTip | QtCore.Qt.WindowStaysOnTopHint) | |||
22 |
|
24 | |||
23 |
# Ensure that |
|
25 | # Ensure that the text edit keeps focus when widget is displayed. | |
24 |
self.setFocusProxy( |
|
26 | self.setFocusProxy(self._text_edit) | |
25 |
|
27 | |||
26 | self.setFrameShadow(QtGui.QFrame.Plain) |
|
28 | self.setFrameShadow(QtGui.QFrame.Plain) | |
27 | self.setFrameShape(QtGui.QFrame.StyledPanel) |
|
29 | self.setFrameShape(QtGui.QFrame.StyledPanel) | |
@@ -29,10 +31,10 b' class CompletionWidget(QtGui.QListWidget):' | |||||
29 | self.itemActivated.connect(self._complete_current) |
|
31 | self.itemActivated.connect(self._complete_current) | |
30 |
|
32 | |||
31 | def eventFilter(self, obj, event): |
|
33 | def eventFilter(self, obj, event): | |
32 |
""" Reimplemented to handle keyboard input and to auto-hide when |
|
34 | """ Reimplemented to handle keyboard input and to auto-hide when the | |
33 |
|
|
35 | text edit loses focus. | |
34 | """ |
|
36 | """ | |
35 |
if obj == self. |
|
37 | if obj == self._text_edit: | |
36 | etype = event.type() |
|
38 | etype = event.type() | |
37 |
|
39 | |||
38 | if etype == QtCore.QEvent.KeyPress: |
|
40 | if etype == QtCore.QEvent.KeyPress: | |
@@ -47,13 +49,13 b' class CompletionWidget(QtGui.QListWidget):' | |||||
47 | elif key in (QtCore.Qt.Key_Up, QtCore.Qt.Key_Down, |
|
49 | elif key in (QtCore.Qt.Key_Up, QtCore.Qt.Key_Down, | |
48 | QtCore.Qt.Key_PageUp, QtCore.Qt.Key_PageDown, |
|
50 | QtCore.Qt.Key_PageUp, QtCore.Qt.Key_PageDown, | |
49 | QtCore.Qt.Key_Home, QtCore.Qt.Key_End): |
|
51 | QtCore.Qt.Key_Home, QtCore.Qt.Key_End): | |
50 |
|
|
52 | self.keyPressEvent(event) | |
51 | return True |
|
53 | return True | |
52 |
|
54 | |||
53 | elif etype == QtCore.QEvent.FocusOut: |
|
55 | elif etype == QtCore.QEvent.FocusOut: | |
54 | self.hide() |
|
56 | self.hide() | |
55 |
|
57 | |||
56 |
return |
|
58 | return super(CompletionWidget, self).eventFilter(obj, event) | |
57 |
|
59 | |||
58 | #-------------------------------------------------------------------------- |
|
60 | #-------------------------------------------------------------------------- | |
59 | # 'QWidget' interface |
|
61 | # 'QWidget' interface | |
@@ -62,21 +64,16 b' class CompletionWidget(QtGui.QListWidget):' | |||||
62 | def hideEvent(self, event): |
|
64 | def hideEvent(self, event): | |
63 | """ Reimplemented to disconnect signal handlers and event filter. |
|
65 | """ Reimplemented to disconnect signal handlers and event filter. | |
64 | """ |
|
66 | """ | |
65 |
|
|
67 | super(CompletionWidget, self).hideEvent(event) | |
66 | parent = self.parent() |
|
68 | self._text_edit.cursorPositionChanged.disconnect(self._update_current) | |
67 | try: |
|
69 | self._text_edit.removeEventFilter(self) | |
68 | parent.cursorPositionChanged.disconnect(self._update_current) |
|
|||
69 | except TypeError: |
|
|||
70 | pass |
|
|||
71 | parent.removeEventFilter(self) |
|
|||
72 |
|
70 | |||
73 | def showEvent(self, event): |
|
71 | def showEvent(self, event): | |
74 | """ Reimplemented to connect signal handlers and event filter. |
|
72 | """ Reimplemented to connect signal handlers and event filter. | |
75 | """ |
|
73 | """ | |
76 |
|
|
74 | super(CompletionWidget, self).showEvent(event) | |
77 | parent = self.parent() |
|
75 | self._text_edit.cursorPositionChanged.connect(self._update_current) | |
78 | parent.cursorPositionChanged.connect(self._update_current) |
|
76 | self._text_edit.installEventFilter(self) | |
79 | parent.installEventFilter(self) |
|
|||
80 |
|
77 | |||
81 | #-------------------------------------------------------------------------- |
|
78 | #-------------------------------------------------------------------------- | |
82 | # 'CompletionWidget' interface |
|
79 | # 'CompletionWidget' interface | |
@@ -86,7 +83,7 b' class CompletionWidget(QtGui.QListWidget):' | |||||
86 | """ Shows the completion widget with 'items' at the position specified |
|
83 | """ Shows the completion widget with 'items' at the position specified | |
87 | by 'cursor'. |
|
84 | by 'cursor'. | |
88 | """ |
|
85 | """ | |
89 |
text_edit = self. |
|
86 | text_edit = self._text_edit | |
90 | point = text_edit.cursorRect(cursor).bottomRight() |
|
87 | point = text_edit.cursorRect(cursor).bottomRight() | |
91 | point = text_edit.mapToGlobal(point) |
|
88 | point = text_edit.mapToGlobal(point) | |
92 | screen_rect = QtGui.QApplication.desktop().availableGeometry(self) |
|
89 | screen_rect = QtGui.QApplication.desktop().availableGeometry(self) | |
@@ -115,7 +112,7 b' class CompletionWidget(QtGui.QListWidget):' | |||||
115 | """ Returns a cursor with text between the start position and the |
|
112 | """ Returns a cursor with text between the start position and the | |
116 | current position selected. |
|
113 | current position selected. | |
117 | """ |
|
114 | """ | |
118 |
cursor = self. |
|
115 | cursor = self._text_edit.textCursor() | |
119 | if cursor.position() >= self._start_position: |
|
116 | if cursor.position() >= self._start_position: | |
120 | cursor.setPosition(self._start_position, |
|
117 | cursor.setPosition(self._start_position, | |
121 | QtGui.QTextCursor.KeepAnchor) |
|
118 | QtGui.QTextCursor.KeepAnchor) |
@@ -46,13 +46,17 b' class MainWindow(QtGui.QMainWindow):' | |||||
46 | def closeEvent(self, event): |
|
46 | def closeEvent(self, event): | |
47 | """ Reimplemented to prompt the user and close the kernel cleanly. |
|
47 | """ Reimplemented to prompt the user and close the kernel cleanly. | |
48 | """ |
|
48 | """ | |
49 | reply = QtGui.QMessageBox.question(self, self.window().windowTitle(), |
|
49 | kernel_manager = self._frontend.kernel_manager | |
50 | 'Close console?', QtGui.QMessageBox.Yes, QtGui.QMessageBox.No) |
|
50 | if kernel_manager and kernel_manager.channels_running: | |
51 | if reply == QtGui.QMessageBox.Yes: |
|
51 | title = self.window().windowTitle() | |
52 | self._frontend.kernel_manager.shutdown_kernel() |
|
52 | reply = QtGui.QMessageBox.question(self, title, | |
53 | event.accept() |
|
53 | 'Close console?', QtGui.QMessageBox.Yes, QtGui.QMessageBox.No) | |
54 | else: |
|
54 | if reply == QtGui.QMessageBox.Yes: | |
55 | event.ignore() |
|
55 | kernel_manager.shutdown_kernel() | |
|
56 | #kernel_manager.stop_channels() | |||
|
57 | event.accept() | |||
|
58 | else: | |||
|
59 | event.ignore() | |||
56 |
|
60 | |||
57 | #----------------------------------------------------------------------------- |
|
61 | #----------------------------------------------------------------------------- | |
58 | # Main entry point |
|
62 | # Main entry point |
General Comments 0
You need to be logged in to leave comments.
Login now