Construct a new console history object.
Private
_cursorPrivate
_editorPrivate
_filteredPrivate
_handleHandle the current kernel changing.
Private
_hasPrivate
_historyPrivate
_isPrivate
_placeholderPrivate
_setReadonly
sessionThe client session used by the foreign handler.
The current editor used by the history manager.
The current editor used by the history widget.
Get whether the console history manager is disposed.
The placeholder text that a history session began with.
Get the previous item in the console history.
The placeholder string that gets temporarily added to the history only for the duration of one history session. If multiple placeholders are sent within a session, only the first one is accepted.
A Promise for console command text or undefined
if unavailable.
Get the next item in the console history.
The placeholder string that gets temporarily added to the history only for the duration of one history session. If multiple placeholders are sent within a session, only the first one is accepted.
A Promise for console command text or undefined
if unavailable.
Protected
onProtected
onPopulate the history collection on history reply from a kernel.
The kernel message history reply.
History entries have the shape: [session: number, line: number, input: string] Contiguous duplicates are stripped out of the API response.
Protected
onAdd a new item to the bottom of history.
The item being added to the bottom of history.
If the item being added is undefined or empty, it is ignored. If the item being added is the same as the last item in history, it is ignored as well so that the console's history will consist of no contiguous repetitions.
Protected
setGenerated using TypeDoc
A console history manager object.