|
@@ -27,6 +27,10 @@ const terminalExtension = {
|
|
|
function activateTerminal(app: Application): void {
|
|
|
|
|
|
let newTerminalId = 'terminal:create-new';
|
|
|
+ let increaseTerminalFontSize = 'terminal:increase-font';
|
|
|
+ let decreaseTerminalFontSize = 'terminal:decrease-font';
|
|
|
+ let toggleTerminalTheme = 'terminal:toggle-theme';
|
|
|
+ let closeAllTerminals = 'terminal:close-all-terminals';
|
|
|
|
|
|
// Track the current active terminal.
|
|
|
let tracker = new WidgetTracker<TerminalWidget>();
|
|
@@ -35,21 +39,107 @@ function activateTerminal(app: Application): void {
|
|
|
activeTerm = widget;
|
|
|
});
|
|
|
|
|
|
- app.commands.add([{
|
|
|
- id: newTerminalId,
|
|
|
- handler: () => {
|
|
|
- let term = new TerminalWidget();
|
|
|
- term.title.closable = true;
|
|
|
- app.shell.addToMainArea(term);
|
|
|
- tracker.addWidget(term);
|
|
|
+ app.commands.add([
|
|
|
+ {
|
|
|
+ id: newTerminalId,
|
|
|
+ handler: () => {
|
|
|
+ let term = new TerminalWidget();
|
|
|
+ term.title.closable = true;
|
|
|
+ app.shell.addToMainArea(term);
|
|
|
+ tracker.addWidget(term);
|
|
|
+ }
|
|
|
+ },
|
|
|
+ {
|
|
|
+ id: increaseTerminalFontSize,
|
|
|
+ handler: increaseFont
|
|
|
+ },
|
|
|
+ {
|
|
|
+ id: decreaseTerminalFontSize,
|
|
|
+ handler: decreaseFont
|
|
|
+ },
|
|
|
+ {
|
|
|
+ id: toggleTerminalTheme,
|
|
|
+ handler: toggleTheme
|
|
|
+ },
|
|
|
+ {
|
|
|
+ id: closeAllTerminals,
|
|
|
+ handler: closeAllTerms
|
|
|
}
|
|
|
- }]);
|
|
|
+]);
|
|
|
app.palette.add([
|
|
|
{
|
|
|
command: newTerminalId,
|
|
|
category: 'Terminal',
|
|
|
text: 'New Terminal',
|
|
|
caption: 'Start a new terminal session'
|
|
|
+ },
|
|
|
+ {
|
|
|
+ command: increaseTerminalFontSize,
|
|
|
+ category: 'Terminal',
|
|
|
+ text: 'Increase Terminal Font Size',
|
|
|
+ },
|
|
|
+ {
|
|
|
+ command: decreaseTerminalFontSize,
|
|
|
+ category: 'Terminal',
|
|
|
+ text: 'Decrease Terminal Font Size',
|
|
|
+ },
|
|
|
+ {
|
|
|
+ command: toggleTerminalTheme,
|
|
|
+ category: 'Terminal',
|
|
|
+ text: 'Toggle Terminal Theme',
|
|
|
+ caption: 'Switch Terminal Background and Font Colors'
|
|
|
+ },
|
|
|
+ {
|
|
|
+ command: closeAllTerminals,
|
|
|
+ category: 'Terminal',
|
|
|
+ text: 'Close All Terminals'
|
|
|
}
|
|
|
]);
|
|
|
+
|
|
|
+ function increaseFont(): void {
|
|
|
+ if (!tracker.isDisposed) {
|
|
|
+ let widgets = tracker.widgets;
|
|
|
+ for (let i = 0; i < widgets.length; i++) {
|
|
|
+ if (widgets[i].fontSize < 72) {
|
|
|
+ widgets[i].fontSize = widgets[i].fontSize + 1;
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ function decreaseFont(): void {
|
|
|
+ if (!tracker.isDisposed) {
|
|
|
+ let widgets = tracker.widgets;
|
|
|
+ for (let i = 0; i < widgets.length; i++) {
|
|
|
+ if (widgets[i].fontSize > 9) {
|
|
|
+ widgets[i].fontSize = widgets[i].fontSize - 1;
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ function toggleTheme(): void {
|
|
|
+ if (!tracker.isDisposed) {
|
|
|
+ let widgets = tracker.widgets;
|
|
|
+ for (let i = 0; i < widgets.length; i++) {
|
|
|
+ if (widgets[i].background === 'black') {
|
|
|
+ widgets[i].background = 'white';
|
|
|
+ widgets[i].color = 'black';
|
|
|
+ }
|
|
|
+ else {
|
|
|
+ widgets[i].background = 'black';
|
|
|
+ widgets[i].color = 'white';
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ function closeAllTerms(): void {
|
|
|
+ if (!tracker.isDisposed) {
|
|
|
+ let widgets = tracker.widgets;
|
|
|
+ for (let i = 0; i < widgets.length; i++) {
|
|
|
+ widgets[i].dispose();
|
|
|
+ }
|
|
|
+ }
|
|
|
+ }
|
|
|
}
|