##// END OF EJS Templates
Fixed the segfaults on application exit. The BracketMatcher, CallTipWidget, and CompletionWidget were using the text control as their parents. This should not be a problem, but for some reason it resulted in problems during shutdown. I suspect that PyQt is bugged and was deleting the C++ objects a second time in the garbage collection phase after they had already been deleted automatically by the C++ layer of Qt.
epatters -
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, parent):
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(parent, (QtGui.QTextEdit, QtGui.QPlainTextEdit))
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.parent().document()
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.parent().textCursor()
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 text_edit = self.parent()
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, parent):
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(parent, (QtGui.QTextEdit, QtGui.QPlainTextEdit))
21 assert isinstance(text_edit, (QtGui.QTextEdit, QtGui.QPlainTextEdit))
22 QtGui.QLabel.__init__(self, parent, QtCore.Qt.ToolTip)
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(parent.document().defaultFont())
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 parent focus
41 """ Reimplemented to hide on certain key presses and on text edit focus
41 changes.
42 changes.
42 """
43 """
43 if obj == self.parent():
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 QtGui.QLabel.eventFilter(self, obj, event)
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 QtGui.QLabel.enterEvent(self, event)
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 parent.cursorPositionChanged.disconnect(self._cursor_position_changed)
88 self._cursor_position_changed)
88 parent.removeEventFilter(self)
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 QtGui.QLabel.leaveEvent(self, event)
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 QtGui.QLabel.paintEvent(self, event)
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 parent.cursorPositionChanged.connect(self._cursor_position_changed)
113 self._cursor_position_changed)
113 parent.installEventFilter(self)
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.parent()
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.parent().document()
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.parent().textCursor()
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, parent):
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(parent, (QtGui.QTextEdit, QtGui.QPlainTextEdit))
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 parent keeps focus when widget is displayed.
25 # Ensure that the text edit keeps focus when widget is displayed.
24 self.setFocusProxy(parent)
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 our
34 """ Reimplemented to handle keyboard input and to auto-hide when the
33 parent loses focus.
35 text edit loses focus.
34 """
36 """
35 if obj == self.parent():
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 QtGui.QListWidget.keyPressEvent(self, event)
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 QtGui.QListWidget.eventFilter(self, obj, event)
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 QtGui.QListWidget.hideEvent(self, event)
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 QtGui.QListWidget.showEvent(self, event)
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.parent()
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.parent().textCursor()
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