##// END OF EJS Templates
Improved the size hint for ConsoleWidget. We now acheive a width of 80 characters, through a mixture of better margin calculation and, well, fudging a little bit.
epatters -
Show More
@@ -113,7 +113,7 b' class ConsoleWidget(QtGui.QWidget):'
113
113
114 # Create the layout and underlying text widget.
114 # Create the layout and underlying text widget.
115 layout = QtGui.QStackedLayout(self)
115 layout = QtGui.QStackedLayout(self)
116 layout.setMargin(0)
116 layout.setContentsMargins(0, 0, 0, 0)
117 self._control = self._create_control(kind)
117 self._control = self._create_control(kind)
118 self._page_control = None
118 self._page_control = None
119 self._splitter = None
119 self._splitter = None
@@ -199,17 +199,21 b' class ConsoleWidget(QtGui.QWidget):'
199 """ Reimplemented to suggest a size that is 80 characters wide and
199 """ Reimplemented to suggest a size that is 80 characters wide and
200 25 lines high.
200 25 lines high.
201 """
201 """
202 style = self.style()
203 opt = QtGui.QStyleOptionHeader()
204 font_metrics = QtGui.QFontMetrics(self.font)
202 font_metrics = QtGui.QFontMetrics(self.font)
205 splitwidth = style.pixelMetric(QtGui.QStyle.PM_SplitterWidth, opt, self)
203 margin = (self._control.frameWidth() +
204 self._control.document().documentMargin()) * 2
205 style = self.style()
206 splitwidth = style.pixelMetric(QtGui.QStyle.PM_SplitterWidth)
206
207
207 width = font_metrics.width(' ') * 80
208 # Despite my best efforts to take the various margins into account, the
208 width += style.pixelMetric(QtGui.QStyle.PM_ScrollBarExtent, opt, self)
209 # width is still coming out a bit too small, so we include a fudge
210 # factor of one character here.
211 width = font_metrics.maxWidth() * 81 + margin
212 width += style.pixelMetric(QtGui.QStyle.PM_ScrollBarExtent)
209 if self._page_style == 'hsplit':
213 if self._page_style == 'hsplit':
210 width = width * 2 + splitwidth
214 width = width * 2 + splitwidth
211
215
212 height = font_metrics.height() * 25
216 height = font_metrics.height() * 25 + margin
213 if self._page_style == 'vsplit':
217 if self._page_style == 'vsplit':
214 height = height * 2 + splitwidth
218 height = height * 2 + splitwidth
215
219
@@ -222,7 +226,7 b' class ConsoleWidget(QtGui.QWidget):'
222 def can_paste(self):
226 def can_paste(self):
223 """ Returns whether text can be pasted from the clipboard.
227 """ Returns whether text can be pasted from the clipboard.
224 """
228 """
225 # Accept only text that can be ASCII encoded.
229 # Only accept text that can be ASCII encoded.
226 if self._control.textInteractionFlags() & QtCore.Qt.TextEditable:
230 if self._control.textInteractionFlags() & QtCore.Qt.TextEditable:
227 text = QtGui.QApplication.clipboard().text()
231 text = QtGui.QApplication.clipboard().text()
228 if not text.isEmpty():
232 if not text.isEmpty():
@@ -800,7 +804,7 b' class ConsoleWidget(QtGui.QWidget):'
800
804
801 # Calculate the number of characters available.
805 # Calculate the number of characters available.
802 width = self._control.viewport().width()
806 width = self._control.viewport().width()
803 char_width = QtGui.QFontMetrics(self.font).width(' ')
807 char_width = QtGui.QFontMetrics(self.font).maxWidth()
804 displaywidth = max(10, (width / char_width) - 1)
808 displaywidth = max(10, (width / char_width) - 1)
805
809
806 # Some degenerate cases.
810 # Some degenerate cases.
General Comments 0
You need to be logged in to leave comments. Login now