Show More
@@ -752,7 +752,10 b' class ConsoleWidget(Configurable, QtGui.QWidget):' | |||
|
752 | 752 | def _create_page_control(self): |
|
753 | 753 | """ Creates and connects the underlying paging widget. |
|
754 | 754 | """ |
|
755 | control = QtGui.QPlainTextEdit() | |
|
755 | if self.kind == 'plain': | |
|
756 | control = QtGui.QPlainTextEdit() | |
|
757 | elif self.kind == 'rich': | |
|
758 | control = QtGui.QTextEdit() | |
|
756 | 759 | control.installEventFilter(self) |
|
757 | 760 | control.setReadOnly(True) |
|
758 | 761 | control.setUndoRedoEnabled(False) |
@@ -1346,32 +1349,38 b' class ConsoleWidget(Configurable, QtGui.QWidget):' | |||
|
1346 | 1349 | else: |
|
1347 | 1350 | self.input_buffer = '' |
|
1348 | 1351 | |
|
1349 | def _page(self, text): | |
|
1350 | """ Displays text using the pager if it exceeds the height of the | |
|
1351 | visible area. | |
|
1352 | def _page(self, text, html=False): | |
|
1353 | """ Displays text using the pager if it exceeds the height of the viewport. | |
|
1354 | ||
|
1355 | Parameters: | |
|
1356 | ----------- | |
|
1357 | html : bool, optional (default False) | |
|
1358 | If set, the text will be interpreted as HTML instead of plain text. | |
|
1352 | 1359 | """ |
|
1353 | if self.paging == 'none': | |
|
1354 | self._append_plain_text(text) | |
|
1355 | else: | |
|
1356 | line_height = QtGui.QFontMetrics(self.font).height() | |
|
1357 | minlines = self._control.viewport().height() / line_height | |
|
1358 | if re.match("(?:[^\n]*\n){%i}" % minlines, text): | |
|
1359 |
|
|
|
1360 |
|
|
|
1360 | line_height = QtGui.QFontMetrics(self.font).height() | |
|
1361 | minlines = self._control.viewport().height() / line_height | |
|
1362 | if self.paging != 'none' and re.match("(?:[^\n]*\n){%i}" % minlines, text): | |
|
1363 | if self.paging == 'custom': | |
|
1364 | self.custom_page_requested.emit(text) | |
|
1365 | else: | |
|
1366 | self._page_control.clear() | |
|
1367 | cursor = self._page_control.textCursor() | |
|
1368 | if html: | |
|
1369 | self._insert_html(cursor, text) | |
|
1361 | 1370 | else: |
|
1362 | self._page_control.clear() | |
|
1363 | cursor = self._page_control.textCursor() | |
|
1364 | 1371 | self._insert_plain_text(cursor, text) |
|
1365 |
|
|
|
1372 | self._page_control.moveCursor(QtGui.QTextCursor.Start) | |
|
1366 | 1373 | |
|
1367 |
|
|
|
1368 |
|
|
|
1369 |
|
|
|
1370 |
|
|
|
1371 |
|
|
|
1372 |
|
|
|
1373 |
|
|
|
1374 |
|
|
|
1374 | self._page_control.viewport().resize(self._control.size()) | |
|
1375 | if self._splitter: | |
|
1376 | self._page_control.show() | |
|
1377 | self._page_control.setFocus() | |
|
1378 | else: | |
|
1379 | self.layout().setCurrentWidget(self._page_control) | |
|
1380 | elif html: | |
|
1381 | self._append_plain_html(text) | |
|
1382 | else: | |
|
1383 | self._append_plain_text(text) | |
|
1375 | 1384 | |
|
1376 | 1385 | def _prompt_finished(self): |
|
1377 | 1386 | """ Called immediately after a prompt is finished, i.e. when some input |
@@ -430,7 +430,13 b' class IPythonWidget(FrontendWidget):' | |||
|
430 | 430 | self.exit_requested.emit() |
|
431 | 431 | |
|
432 | 432 | def _handle_payload_page(self, item): |
|
433 | self._page(item['text']) | |
|
433 | # Since the plain text widget supports only a very small subset of HTML | |
|
434 | # and we have no control over the HTML source, we only page HTML | |
|
435 | # payloads in the rich text widget. | |
|
436 | if item['html'] and self.kind == 'rich': | |
|
437 | self._page(item['html'], html=True) | |
|
438 | else: | |
|
439 | self._page(item['text'], html=False) | |
|
434 | 440 | |
|
435 | 441 | #------ Trait change handlers --------------------------------------------- |
|
436 | 442 |
General Comments 0
You need to be logged in to leave comments.
Login now