|
Public Member Functions |
| SourceEditorWidget (string languageMimeType, CommandHistoryStore commandHistoryStore, Shell shell) |
void | SetBufferAndIndent (string code) |
void | SetCommand (int commandNumber, string commandText) |
| Must be called whenever a command is selected, by the user clicking in the "command history" table. And not when it is selected by AltUpArrow and AltDownArrow.
|
string | GetAndExecuteCommand () |
| Must be called whenever a command is executed.
|
Public Attributes |
ObservableWriterStream | StdOutput = new ObservableWriterStream() |
Protected Member Functions |
override bool | OnKeyPressEvent (Gdk.EventKey evnt) |
Private Member Functions |
void | SetAndSelectCommand (int commandNumber) |
| Sets a command and make CommandHistoryStore set it (highlight it).
|
void | AutoCompletion () |
Private Attributes |
SourceBuffer | SourceBuffer |
CommandHistoryStore | _commandHistoryStore |
Shell | _shell |
AutoCompletion | _autoCompletion |
int | _currentCommandNumber = -1 |
string | _nonHistoryCommand = "" |