Construct a new console history object.
Handle the current kernel changing.
The 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.
Dispose of the resources held by the console history manager.
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.
Handle an edge requested signal.
Populate 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.
Handle a text change signal from the editor.
Add 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.
Reset the history navigation state, i.e., start a new history session.
Set the filter data.
The string to use when filtering the data.
Generated using TypeDoc
A console history manager object.