Merge from vscode b12f623603e2fc1c5b3037115fa37c1a6acc4165 (#6760)

This commit is contained in:
Anthony Dresser
2019-08-15 02:19:31 -07:00
committed by GitHub
parent 4966ed8b42
commit 58bfba4b47
161 changed files with 2072 additions and 1317 deletions

View File

@@ -63,14 +63,14 @@ export class LinesLayout {
* @param heightInPx The height of the whitespace, in pixels.
* @return An id that can be used later to mutate or delete the whitespace
*/
public insertWhitespace(afterLineNumber: number, ordinal: number, heightInPx: number, minWidth: number): number {
public insertWhitespace(afterLineNumber: number, ordinal: number, heightInPx: number, minWidth: number): string {
return this._whitespaces.insertWhitespace(afterLineNumber, ordinal, heightInPx, minWidth);
}
/**
* Change properties associated with a certain whitespace.
*/
public changeWhitespace(id: number, newAfterLineNumber: number, newHeight: number): boolean {
public changeWhitespace(id: string, newAfterLineNumber: number, newHeight: number): boolean {
return this._whitespaces.changeWhitespace(id, newAfterLineNumber, newHeight);
}
@@ -80,7 +80,7 @@ export class LinesLayout {
* @param id The whitespace to remove
* @return Returns true if the whitespace is found and it is removed.
*/
public removeWhitespace(id: number): boolean {
public removeWhitespace(id: string): boolean {
return this._whitespaces.removeWhitespace(id);
}

View File

@@ -173,13 +173,13 @@ export class ViewLayout extends Disposable implements IViewLayout {
// ---- IVerticalLayoutProvider
public addWhitespace(afterLineNumber: number, ordinal: number, height: number, minWidth: number): number {
public addWhitespace(afterLineNumber: number, ordinal: number, height: number, minWidth: number): string {
return this._linesLayout.insertWhitespace(afterLineNumber, ordinal, height, minWidth);
}
public changeWhitespace(id: number, newAfterLineNumber: number, newHeight: number): boolean {
public changeWhitespace(id: string, newAfterLineNumber: number, newHeight: number): boolean {
return this._linesLayout.changeWhitespace(id, newAfterLineNumber, newHeight);
}
public removeWhitespace(id: number): boolean {
public removeWhitespace(id: string): boolean {
return this._linesLayout.removeWhitespace(id);
}
public getVerticalOffsetForLineNumber(lineNumber: number): number {

View File

@@ -3,8 +3,10 @@
* Licensed under the Source EULA. See License.txt in the project root for license information.
*--------------------------------------------------------------------------------------------*/
import * as strings from 'vs/base/common/strings';
export interface IEditorWhitespace {
readonly id: number;
readonly id: string;
readonly afterLineNumber: number;
readonly heightInLines: number;
}
@@ -15,6 +17,10 @@ export interface IEditorWhitespace {
*/
export class WhitespaceComputer {
private static INSTANCE_COUNT = 0;
private readonly _instanceId: string;
/**
* heights[i] is the height in pixels for whitespace at index i
*/
@@ -48,7 +54,7 @@ export class WhitespaceComputer {
/**
* ids[i] is the whitespace id of whitespace at index i
*/
private readonly _ids: number[];
private readonly _ids: string[];
/**
* index at which a whitespace is positioned (inside heights, afterLineNumbers, prefixSum members)
@@ -65,6 +71,7 @@ export class WhitespaceComputer {
private _minWidth: number;
constructor() {
this._instanceId = strings.singleLetterHash(++WhitespaceComputer.INSTANCE_COUNT);
this._heights = [];
this._minWidths = [];
this._ids = [];
@@ -113,21 +120,20 @@ export class WhitespaceComputer {
* @param heightInPx The height of the whitespace, in pixels.
* @return An id that can be used later to mutate or delete the whitespace
*/
public insertWhitespace(afterLineNumber: number, ordinal: number, heightInPx: number, minWidth: number): number {
public insertWhitespace(afterLineNumber: number, ordinal: number, heightInPx: number, minWidth: number): string {
afterLineNumber = afterLineNumber | 0;
ordinal = ordinal | 0;
heightInPx = heightInPx | 0;
minWidth = minWidth | 0;
let id = (++this._lastWhitespaceId);
let id = this._instanceId + (++this._lastWhitespaceId);
let insertionIndex = WhitespaceComputer.findInsertionIndex(this._afterLineNumbers, afterLineNumber, this._ordinals, ordinal);
this._insertWhitespaceAtIndex(id, insertionIndex, afterLineNumber, ordinal, heightInPx, minWidth);
this._minWidth = -1; /* marker for not being computed */
return id;
}
private _insertWhitespaceAtIndex(id: number, insertIndex: number, afterLineNumber: number, ordinal: number, heightInPx: number, minWidth: number): void {
id = id | 0;
private _insertWhitespaceAtIndex(id: string, insertIndex: number, afterLineNumber: number, ordinal: number, heightInPx: number, minWidth: number): void {
insertIndex = insertIndex | 0;
afterLineNumber = afterLineNumber | 0;
ordinal = ordinal | 0;
@@ -150,15 +156,14 @@ export class WhitespaceComputer {
}
}
this._whitespaceId2Index[id.toString()] = insertIndex;
this._whitespaceId2Index[id] = insertIndex;
this._prefixSumValidIndex = Math.min(this._prefixSumValidIndex, insertIndex - 1);
}
/**
* Change properties associated with a certain whitespace.
*/
public changeWhitespace(id: number, newAfterLineNumber: number, newHeight: number): boolean {
id = id | 0;
public changeWhitespace(id: string, newAfterLineNumber: number, newHeight: number): boolean {
newAfterLineNumber = newAfterLineNumber | 0;
newHeight = newHeight | 0;
@@ -175,13 +180,11 @@ export class WhitespaceComputer {
* @param newHeightInPx The new height of the whitespace, in pixels
* @return Returns true if the whitespace is found and if the new height is different than the old height
*/
public changeWhitespaceHeight(id: number, newHeightInPx: number): boolean {
id = id | 0;
public changeWhitespaceHeight(id: string, newHeightInPx: number): boolean {
newHeightInPx = newHeightInPx | 0;
let sid = id.toString();
if (this._whitespaceId2Index.hasOwnProperty(sid)) {
let index = this._whitespaceId2Index[sid];
if (this._whitespaceId2Index.hasOwnProperty(id)) {
let index = this._whitespaceId2Index[id];
if (this._heights[index] !== newHeightInPx) {
this._heights[index] = newHeightInPx;
this._prefixSumValidIndex = Math.min(this._prefixSumValidIndex, index - 1);
@@ -198,13 +201,11 @@ export class WhitespaceComputer {
* @param newAfterLineNumber The new line number the whitespace will follow
* @return Returns true if the whitespace is found and if the new line number is different than the old line number
*/
public changeWhitespaceAfterLineNumber(id: number, newAfterLineNumber: number): boolean {
id = id | 0;
public changeWhitespaceAfterLineNumber(id: string, newAfterLineNumber: number): boolean {
newAfterLineNumber = newAfterLineNumber | 0;
let sid = id.toString();
if (this._whitespaceId2Index.hasOwnProperty(sid)) {
let index = this._whitespaceId2Index[sid];
if (this._whitespaceId2Index.hasOwnProperty(id)) {
let index = this._whitespaceId2Index[id];
if (this._afterLineNumbers[index] !== newAfterLineNumber) {
// `afterLineNumber` changed for this whitespace
@@ -236,14 +237,10 @@ export class WhitespaceComputer {
* @param id The whitespace to remove
* @return Returns true if the whitespace is found and it is removed.
*/
public removeWhitespace(id: number): boolean {
id = id | 0;
let sid = id.toString();
if (this._whitespaceId2Index.hasOwnProperty(sid)) {
let index = this._whitespaceId2Index[sid];
delete this._whitespaceId2Index[sid];
public removeWhitespace(id: string): boolean {
if (this._whitespaceId2Index.hasOwnProperty(id)) {
let index = this._whitespaceId2Index[id];
delete this._whitespaceId2Index[id];
this._removeWhitespaceAtIndex(index);
this._minWidth = -1; /* marker for not being computed */
return true;
@@ -459,7 +456,7 @@ export class WhitespaceComputer {
* @param index The index of the whitespace.
* @return `id` of whitespace at `index`.
*/
public getIdForWhitespaceIndex(index: number): number {
public getIdForWhitespaceIndex(index: number): string {
index = index | 0;
return this._ids[index];