src/SelectionManager.ts

   1 /**
   2  * @license MIT
   3  */
   4
   5 import * as Mouse from './utils/Mouse';
   6 import * as Browser from './utils/Browser';
   7 import { CharMeasure } from './utils/CharMeasure';
   8 import { CircularList } from './utils/CircularList';
   9 import { EventEmitter } from './EventEmitter';
  10 import { ITerminal } from './Interfaces';
  11 import { SelectionModel } from './SelectionModel';
  12 import { translateBufferLineToString } from './utils/BufferLine';
  13
  14 /**
  15  * The number of pixels the mouse needs to be above or below the viewport in
  16  * order to scroll at the maximum speed.
  17  */
  18 const DRAG_SCROLL_MAX_THRESHOLD = 50;
  19
  20 /**
  21  * The maximum scrolling speed
  22  */
  23 const DRAG_SCROLL_MAX_SPEED = 15;
  24
  25 /**
  26  * The number of milliseconds between drag scroll updates.
  27  */
  28 const DRAG_SCROLL_INTERVAL = 50;
  29
  30 /**
  31  * The amount of time before mousedown events are no longer stacked to create
  32  * double/triple click events.
  33  */
  34 const CLEAR_MOUSE_DOWN_TIME = 400;
  35
  36 /**
  37  * The number of pixels in each direction that the mouse must move before
  38  * mousedown events are no longer stacked to create double/triple click events.
  39  */
  40 const CLEAR_MOUSE_DISTANCE = 10;
  41
  42 /**
  43  * A string containing all characters that are considered word separated by the
  44  * double click to select work logic.
  45  */
  46 const WORD_SEPARATORS = ' ()[]{}:\'"';
  47
  48 // TODO: Move these constants elsewhere, they belong in a buffer or buffer
  49 //       data/line class.
  50 const LINE_DATA_CHAR_INDEX = 1;
  51 const LINE_DATA_WIDTH_INDEX = 2;
  52
  53 const NON_BREAKING_SPACE_CHAR = String.fromCharCode(160);
  54 const ALL_NON_BREAKING_SPACE_REGEX = new RegExp(NON_BREAKING_SPACE_CHAR, 'g');
  55
  56 /**
  57  * Represents a position of a word on a line.
  58  */
  59 interface IWordPosition {
  60   start: number;
  61   length: number;
  62 }
  63
  64 /**
  65  * A selection mode, this drives how the selection behaves on mouse move.
  66  */
  67 enum SelectionMode {
  68   NORMAL,
  69   WORD,
  70   LINE
  71 }
  72
  73 /**
  74  * A class that manages the selection of the terminal. With help from
  75  * SelectionModel, SelectionManager handles with all logic associated with
  76  * dealing with the selection, including handling mouse interaction, wide
  77  * characters and fetching the actual text within the selection. Rendering is
  78  * not handled by the SelectionManager but a 'refresh' event is fired when the
  79  * selection is ready to be redrawn.
  80  */
  81 export class SelectionManager extends EventEmitter {
  82   protected _model: SelectionModel;
  83
  84   /**
  85    * The amount to scroll every drag scroll update (depends on how far the mouse
  86    * drag is above or below the terminal).
  87    */
  88   private _dragScrollAmount: number;
  89
  90   /**
  91    * The last time the mousedown event fired, this is used to track double and
  92    * triple clicks.
  93    */
  94   private _lastMouseDownTime: number;
  95
  96   /**
  97    * The last position the mouse was clicked [x, y].
  98    */
  99   private _lastMousePosition: [number, number];
 100
 101   /**
 102    * The number of clicks of the mousedown event. This is used to keep track of
 103    * double and triple clicks.
 104    */
 105   private _clickCount: number;
 106
 107   /**
 108    * The current selection mode.
 109    */
 110   private _activeSelectionMode: SelectionMode;
 111
 112   /**
 113    * A setInterval timer that is active while the mouse is down whose callback
 114    * scrolls the viewport when necessary.
 115    */
 116   private _dragScrollIntervalTimer: NodeJS.Timer;
 117
 118   /**
 119    * The animation frame ID used for refreshing the selection.
 120    */
 121   private _refreshAnimationFrame: number;
 122
 123   private _bufferTrimListener: any;
 124   private _mouseMoveListener: EventListener;
 125   private _mouseDownListener: EventListener;
 126   private _mouseUpListener: EventListener;
 127
 128   constructor(
 129     private _terminal: ITerminal,
 130     private _buffer: CircularList<any>,
 131     private _rowContainer: HTMLElement,
 132     private _charMeasure: CharMeasure
 133   ) {
 134     super();
 135     this._initListeners();
 136     this.enable();
 137
 138     this._model = new SelectionModel(_terminal);
 139     this._lastMouseDownTime = 0;
 140     this._activeSelectionMode = SelectionMode.NORMAL;
 141   }
 142
 143   /**
 144    * Initializes listener variables.
 145    */
 146   private _initListeners() {
 147     this._bufferTrimListener = (amount: number) => this._onTrim(amount);
 148     this._mouseMoveListener = event => this._onMouseMove(<MouseEvent>event);
 149     this._mouseDownListener = event => this._onMouseDown(<MouseEvent>event);
 150     this._mouseUpListener = event => this._onMouseUp(<MouseEvent>event);
 151   }
 152
 153   /**
 154    * Disables the selection manager. This is useful for when terminal mouse
 155    * are enabled.
 156    */
 157   public disable() {
 158     this.clearSelection();
 159     this._buffer.off('trim', this._bufferTrimListener);
 160     this._rowContainer.removeEventListener('mousedown', this._mouseDownListener);
 161   }
 162
 163   /**
 164    * Enable the selection manager.
 165    */
 166   public enable() {
 167     // Only adjust the selection on trim, shiftElements is rarely used (only in
 168     // reverseIndex) and delete in a splice is only ever used when the same
 169     // number of elements was just added. Given this is could actually be
 170     // beneficial to leave the selection as is for these cases.
 171     this._buffer.on('trim', this._bufferTrimListener);
 172     this._rowContainer.addEventListener('mousedown', this._mouseDownListener);
 173   }
 174
 175   /**
 176    * Sets the active buffer, this should be called when the alt buffer is
 177    * switched in or out.
 178    * @param buffer The active buffer.
 179    */
 180   public setBuffer(buffer: CircularList<any>): void {
 181     this._buffer = buffer;
 182   }
 183
 184   public get selectionStart(): [number, number] { return this._model.finalSelectionStart; }
 185   public get selectionEnd(): [number, number] { return this._model.finalSelectionEnd; }
 186
 187   /**
 188    * Gets whether there is an active text selection.
 189    */
 190   public get hasSelection(): boolean {
 191     const start = this._model.finalSelectionStart;
 192     const end = this._model.finalSelectionEnd;
 193     if (!start || !end) {
 194       return false;
 195     }
 196     return start[0] !== end[0] || start[1] !== end[1];
 197   }
 198
 199   /**
 200    * Gets the text currently selected.
 201    */
 202   public get selectionText(): string {
 203     const start = this._model.finalSelectionStart;
 204     const end = this._model.finalSelectionEnd;
 205     if (!start || !end) {
 206       return '';
 207     }
 208
 209     // Get first row
 210     const startRowEndCol = start[1] === end[1] ? end[0] : null;
 211     let result: string[] = [];
 212     result.push(translateBufferLineToString(this._buffer.get(start[1]), true, start[0], startRowEndCol));
 213
 214     // Get middle rows
 215     for (let i = start[1] + 1; i <= end[1] - 1; i++) {
 216       const bufferLine = this._buffer.get(i);
 217       const lineText = translateBufferLineToString(bufferLine, true);
 218       if (bufferLine.isWrapped) {
 219         result[result.length - 1] += lineText;
 220       } else {
 221         result.push(lineText);
 222       }
 223     }
 224
 225     // Get final row
 226     if (start[1] !== end[1]) {
 227       const bufferLine = this._buffer.get(end[1]);
 228       const lineText = translateBufferLineToString(bufferLine, true, 0, end[0]);
 229       if (bufferLine.isWrapped) {
 230         result[result.length - 1] += lineText;
 231       } else {
 232         result.push(lineText);
 233       }
 234     }
 235
 236     // Format string by replacing non-breaking space chars with regular spaces
 237     // and joining the array into a multi-line string.
 238     const formattedResult = result.map(line => {
 239       return line.replace(ALL_NON_BREAKING_SPACE_REGEX, ' ');
 240     }).join('\n');
 241
 242     return formattedResult;
 243   }
 244
 245   /**
 246    * Clears the current terminal selection.
 247    */
 248   public clearSelection(): void {
 249     this._model.clearSelection();
 250     this._removeMouseDownListeners();
 251     this.refresh();
 252   }
 253
 254   /**
 255    * Queues a refresh, redrawing the selection on the next opportunity.
 256    * @param isNewSelection Whether the selection should be registered as a new
 257    * selection on Linux.
 258    */
 259   public refresh(isNewSelection?: boolean): void {
 260     // Queue the refresh for the renderer
 261     if (!this._refreshAnimationFrame) {
 262       this._refreshAnimationFrame = window.requestAnimationFrame(() => this._refresh());
 263     }
 264
 265     // If the platform is Linux and the refresh call comes from a mouse event,
 266     // we need to update the selection for middle click to paste selection.
 267     if (Browser.isLinux && isNewSelection) {
 268       const selectionText = this.selectionText;
 269       if (selectionText.length) {
 270         this.emit('newselection', this.selectionText);
 271       }
 272     }
 273   }
 274
 275   /**
 276    * Fires the refresh event, causing consumers to pick it up and redraw the
 277    * selection state.
 278    */
 279   private _refresh(): void {
 280     this._refreshAnimationFrame = null;
 281     this.emit('refresh', { start: this._model.finalSelectionStart, end: this._model.finalSelectionEnd });
 282   }
 283
 284   /**
 285    * Selects all text within the terminal.
 286    */
 287   public selectAll(): void {
 288     this._model.isSelectAllActive = true;
 289     this.refresh();
 290   }
 291
 292   /**
 293    * Handle the buffer being trimmed, adjust the selection position.
 294    * @param amount The amount the buffer is being trimmed.
 295    */
 296   private _onTrim(amount: number) {
 297     const needsRefresh = this._model.onTrim(amount);
 298     if (needsRefresh) {
 299       this.refresh();
 300     }
 301   }
 302
 303   /**
 304    * Gets the 0-based [x, y] buffer coordinates of the current mouse event.
 305    * @param event The mouse event.
 306    */
 307   private _getMouseBufferCoords(event: MouseEvent): [number, number] {
 308     const coords = Mouse.getCoords(event, this._rowContainer, this._charMeasure, this._terminal.cols, this._terminal.rows, true);
 309     // Convert to 0-based
 310     coords[0]--;
 311     coords[1]--;
 312     // Convert viewport coords to buffer coords
 313     coords[1] += this._terminal.ydisp;
 314     return coords;
 315   }
 316
 317   /**
 318    * Gets the amount the viewport should be scrolled based on how far out of the
 319    * terminal the mouse is.
 320    * @param event The mouse event.
 321    */
 322   private _getMouseEventScrollAmount(event: MouseEvent): number {
 323     let offset = Mouse.getCoordsRelativeToElement(event, this._rowContainer)[1];
 324     const terminalHeight = this._terminal.rows * this._charMeasure.height;
 325     if (offset >= 0 && offset <= terminalHeight) {
 326       return 0;
 327     }
 328     if (offset > terminalHeight) {
 329       offset -= terminalHeight;
 330     }
 331
 332     offset = Math.min(Math.max(offset, -DRAG_SCROLL_MAX_THRESHOLD), DRAG_SCROLL_MAX_THRESHOLD);
 333     offset /= DRAG_SCROLL_MAX_THRESHOLD;
 334     return (offset / Math.abs(offset)) + Math.round(offset * (DRAG_SCROLL_MAX_SPEED - 1));
 335   }
 336
 337   /**
 338    * Handles te mousedown event, setting up for a new selection.
 339    * @param event The mousedown event.
 340    */
 341   private _onMouseDown(event: MouseEvent) {
 342     // Only action the primary button
 343     if (event.button !== 0) {
 344       return;
 345     }
 346
 347     // Tell the browser not to start a regular selection
 348     event.preventDefault();
 349
 350     // Reset drag scroll state
 351     this._dragScrollAmount = 0;
 352
 353     this._setMouseClickCount(event);
 354
 355     if (event.shiftKey) {
 356       this._onShiftClick(event);
 357     } else {
 358       if (this._clickCount === 1) {
 359           this._onSingleClick(event);
 360       } else if (this._clickCount === 2) {
 361           this._onDoubleClick(event);
 362       } else if (this._clickCount === 3) {
 363           this._onTripleClick(event);
 364       }
 365     }
 366
 367     this._addMouseDownListeners();
 368     this.refresh(true);
 369   }
 370
 371   /**
 372    * Adds listeners when mousedown is triggered.
 373    */
 374   private _addMouseDownListeners(): void {
 375     // Listen on the document so that dragging outside of viewport works
 376     this._rowContainer.ownerDocument.addEventListener('mousemove', this._mouseMoveListener);
 377     this._rowContainer.ownerDocument.addEventListener('mouseup', this._mouseUpListener);
 378     this._dragScrollIntervalTimer = setInterval(() => this._dragScroll(), DRAG_SCROLL_INTERVAL);
 379   }
 380
 381   /**
 382    * Removes the listeners that are registered when mousedown is triggered.
 383    */
 384   private _removeMouseDownListeners(): void {
 385     this._rowContainer.ownerDocument.removeEventListener('mousemove', this._mouseMoveListener);
 386     this._rowContainer.ownerDocument.removeEventListener('mouseup', this._mouseUpListener);
 387     clearInterval(this._dragScrollIntervalTimer);
 388     this._dragScrollIntervalTimer = null;
 389   }
 390
 391   /**
 392    * Performs a shift click, setting the selection end position to the mouse
 393    * position.
 394    * @param event The mouse event.
 395    */
 396   private _onShiftClick(event: MouseEvent): void {
 397     if (this._model.selectionStart) {
 398       this._model.selectionEnd = this._getMouseBufferCoords(event);
 399     }
 400   }
 401
 402   /**
 403    * Performs a single click, resetting relevant state and setting the selection
 404    * start position.
 405    * @param event The mouse event.
 406    */
 407   private _onSingleClick(event: MouseEvent): void {
 408     this._model.selectionStartLength = 0;
 409     this._model.isSelectAllActive = false;
 410     this._activeSelectionMode = SelectionMode.NORMAL;
 411     this._model.selectionStart = this._getMouseBufferCoords(event);
 412     if (this._model.selectionStart) {
 413       this._model.selectionEnd = null;
 414       // If the mouse is over the second half of a wide character, adjust the
 415       // selection to cover the whole character
 416       const char = this._buffer.get(this._model.selectionStart[1])[this._model.selectionStart[0]];
 417       if (char[LINE_DATA_WIDTH_INDEX] === 0) {
 418         this._model.selectionStart[0]++;
 419       }
 420     }
 421   }
 422
 423   /**
 424    * Performs a double click, selecting the current work.
 425    * @param event The mouse event.
 426    */
 427   private _onDoubleClick(event: MouseEvent): void {
 428     const coords = this._getMouseBufferCoords(event);
 429     if (coords) {
 430       this._activeSelectionMode = SelectionMode.WORD;
 431       this._selectWordAt(coords);
 432     }
 433   }
 434
 435   /**
 436    * Performs a triple click, selecting the current line and activating line
 437    * select mode.
 438    * @param event The mouse event.
 439    */
 440   private _onTripleClick(event: MouseEvent): void {
 441     const coords = this._getMouseBufferCoords(event);
 442     if (coords) {
 443       this._activeSelectionMode = SelectionMode.LINE;
 444       this._selectLineAt(coords[1]);
 445     }
 446   }
 447
 448   /**
 449    * Sets the number of clicks for the current mousedown event based on the time
 450    * and position of the last mousedown event.
 451    * @param event The mouse event.
 452    */
 453   private _setMouseClickCount(event: MouseEvent): void {
 454     let currentTime = (new Date()).getTime();
 455     if (currentTime - this._lastMouseDownTime > CLEAR_MOUSE_DOWN_TIME || this._distanceFromLastMousePosition(event) > CLEAR_MOUSE_DISTANCE) {
 456       this._clickCount = 0;
 457     }
 458     this._lastMouseDownTime = currentTime;
 459     this._lastMousePosition = [event.pageX, event.pageY];
 460     this._clickCount++;
 461   }
 462
 463   /**
 464    * Gets the maximum number of pixels in each direction the mouse has moved.
 465    * @param event The mouse event.
 466    */
 467   private _distanceFromLastMousePosition(event: MouseEvent): number {
 468     const result = Math.max(
 469         Math.abs(this._lastMousePosition[0] - event.pageX),
 470         Math.abs(this._lastMousePosition[1] - event.pageY));
 471     return result;
 472   }
 473
 474   /**
 475    * Handles the mousemove event when the mouse button is down, recording the
 476    * end of the selection and refreshing the selection.
 477    * @param event The mousemove event.
 478    */
 479   private _onMouseMove(event: MouseEvent) {
 480     // Record the previous position so we know whether to redraw the selection
 481     // at the end.
 482     const previousSelectionEnd = this._model.selectionEnd ? [this._model.selectionEnd[0], this._model.selectionEnd[1]] : null;
 483
 484     // Set the initial selection end based on the mouse coordinates
 485     this._model.selectionEnd = this._getMouseBufferCoords(event);
 486
 487     // Select the entire line if line select mode is active.
 488     if (this._activeSelectionMode === SelectionMode.LINE) {
 489       if (this._model.selectionEnd[1] < this._model.selectionStart[1]) {
 490         this._model.selectionEnd[0] = 0;
 491       } else {
 492         this._model.selectionEnd[0] = this._terminal.cols;
 493       }
 494     } else if (this._activeSelectionMode === SelectionMode.WORD) {
 495       this._selectToWordAt(this._model.selectionEnd);
 496     }
 497
 498     // Determine the amount of scrolling that will happen.
 499     this._dragScrollAmount = this._getMouseEventScrollAmount(event);
 500
 501     // If the cursor was above or below the viewport, make sure it's at the
 502     // start or end of the viewport respectively.
 503     if (this._dragScrollAmount > 0) {
 504       this._model.selectionEnd[0] = this._terminal.cols - 1;
 505     } else if (this._dragScrollAmount < 0) {
 506       this._model.selectionEnd[0] = 0;
 507     }
 508
 509     // If the character is a wide character include the cell to the right in the
 510     // selection. Note that selections at the very end of the line will never
 511     // have a character.
 512     if (this._model.selectionEnd[1] < this._buffer.length) {
 513       const char = this._buffer.get(this._model.selectionEnd[1])[this._model.selectionEnd[0]];
 514       if (char && char[2] === 0) {
 515         this._model.selectionEnd[0]++;
 516       }
 517     }
 518
 519     // Only draw here if the selection changes.
 520     if (!previousSelectionEnd ||
 521         previousSelectionEnd[0] !== this._model.selectionEnd[0] ||
 522         previousSelectionEnd[1] !== this._model.selectionEnd[1]) {
 523       this.refresh(true);
 524     }
 525   }
 526
 527   /**
 528    * The callback that occurs every DRAG_SCROLL_INTERVAL ms that does the
 529    * scrolling of the viewport.
 530    */
 531   private _dragScroll() {
 532     if (this._dragScrollAmount) {
 533       this._terminal.scrollDisp(this._dragScrollAmount, false);
 534       // Re-evaluate selection
 535       if (this._dragScrollAmount > 0) {
 536         this._model.selectionEnd = [this._terminal.cols - 1, this._terminal.ydisp + this._terminal.rows];
 537       } else {
 538         this._model.selectionEnd = [0, this._terminal.ydisp];
 539       }
 540       this.refresh();
 541     }
 542   }
 543
 544   /**
 545    * Handles the mouseup event, removing the mousedown listeners.
 546    * @param event The mouseup event.
 547    */
 548   private _onMouseUp(event: MouseEvent) {
 549     this._removeMouseDownListeners();
 550   }
 551
 552   /**
 553    * Converts a viewport column to the character index on the buffer line, the
 554    * latter takes into account wide characters.
 555    * @param coords The coordinates to find the 2 index for.
 556    */
 557   private _convertViewportColToCharacterIndex(bufferLine: any, coords: [number, number]): number {
 558     let charIndex = coords[0];
 559     for (let i = 0; coords[0] >= i; i++) {
 560       const char = bufferLine[i];
 561       if (char[LINE_DATA_WIDTH_INDEX] === 0) {
 562         charIndex--;
 563       }
 564     }
 565     return charIndex;
 566   }
 567
 568   public setSelection(col: number, row: number, length: number): void {
 569     this._model.clearSelection();
 570     this._removeMouseDownListeners();
 571     this._model.selectionStart = [col, row];
 572     this._model.selectionStartLength = length;
 573     this.refresh();
 574   }
 575
 576   /**
 577    * Gets positional information for the word at the coordinated specified.
 578    * @param coords The coordinates to get the word at.
 579    */
 580   private _getWordAt(coords: [number, number]): IWordPosition {
 581     const bufferLine = this._buffer.get(coords[1]);
 582     const line = translateBufferLineToString(bufferLine, false);
 583
 584     // Get actual index, taking into consideration wide characters
 585     let endIndex = this._convertViewportColToCharacterIndex(bufferLine, coords);
 586     let startIndex = endIndex;
 587
 588     // Record offset to be used later
 589     const charOffset = coords[0] - startIndex;
 590     let leftWideCharCount = 0;
 591     let rightWideCharCount = 0;
 592
 593     if (line.charAt(startIndex) === ' ') {
 594       // Expand until non-whitespace is hit
 595       while (startIndex > 0 && line.charAt(startIndex - 1) === ' ') {
 596         startIndex--;
 597       }
 598       while (endIndex < line.length && line.charAt(endIndex + 1) === ' ') {
 599         endIndex++;
 600       }
 601     } else {
 602       // Expand until whitespace is hit. This algorithm works by scanning left
 603       // and right from the starting position, keeping both the index format
 604       // (line) and the column format (bufferLine) in sync. When a wide
 605       // character is hit, it is recorded and the column index is adjusted.
 606       let startCol = coords[0];
 607       let endCol = coords[0];
 608       // Consider the initial position, skip it and increment the wide char
 609       // variable
 610       if (bufferLine[startCol][LINE_DATA_WIDTH_INDEX] === 0) {
 611         leftWideCharCount++;
 612         startCol--;
 613       }
 614       if (bufferLine[endCol][LINE_DATA_WIDTH_INDEX] === 2) {
 615         rightWideCharCount++;
 616         endCol++;
 617       }
 618       // Expand the string in both directions until a space is hit
 619       while (startIndex > 0 && !this._isCharWordSeparator(line.charAt(startIndex - 1))) {
 620         if (bufferLine[startCol - 1][LINE_DATA_WIDTH_INDEX] === 0) {
 621           // If the next character is a wide char, record it and skip the column
 622           leftWideCharCount++;
 623           startCol--;
 624         }
 625         startIndex--;
 626         startCol--;
 627       }
 628       while (endIndex + 1 < line.length && !this._isCharWordSeparator(line.charAt(endIndex + 1))) {
 629         if (bufferLine[endCol + 1][LINE_DATA_WIDTH_INDEX] === 2) {
 630           // If the next character is a wide char, record it and skip the column
 631           rightWideCharCount++;
 632           endCol++;
 633         }
 634         endIndex++;
 635         endCol++;
 636       }
 637     }
 638
 639     const start = startIndex + charOffset - leftWideCharCount;
 640     const length = Math.min(endIndex - startIndex + leftWideCharCount + rightWideCharCount + 1/*include endIndex char*/, this._terminal.cols);
 641     return {start, length};
 642   }
 643
 644   /**
 645    * Selects the word at the coordinates specified.
 646    * @param coords The coordinates to get the word at.
 647    */
 648   protected _selectWordAt(coords: [number, number]): void {
 649     const wordPosition = this._getWordAt(coords);
 650     this._model.selectionStart = [wordPosition.start, coords[1]];
 651     this._model.selectionStartLength = wordPosition.length;
 652   }
 653
 654   /**
 655    * Sets the selection end to the word at the coordinated specified.
 656    * @param coords The coordinates to get the word at.
 657    */
 658   private _selectToWordAt(coords: [number, number]): void {
 659     const wordPosition = this._getWordAt(coords);
 660     this._model.selectionEnd = [this._model.areSelectionValuesReversed() ? wordPosition.start : (wordPosition.start + wordPosition.length), coords[1]];
 661   }
 662
 663   /**
 664    * Gets whether the character is considered a word separator by the select
 665    * word logic.
 666    * @param char The character to check.
 667    */
 668   private _isCharWordSeparator(char: string): boolean {
 669     return WORD_SEPARATORS.indexOf(char) >= 0;
 670   }
 671
 672   /**
 673    * Selects the line specified.
 674    * @param line The line index.
 675    */
 676   protected _selectLineAt(line: number): void {
 677     this._model.selectionStart = [0, line];
 678     this._model.selectionStartLength = this._terminal.cols;
 679   }
 680 }