ckaczor/azuredatastudio
1
0
Fork 0
mirror of https://github.com/ckaczor/azuredatastudio.git synced 2026-02-16 10:58:30 -05:00
Code Issues Packages Projects Releases Wiki Activity

Merge from vscode 8a997f7321ae6612fc0e6eb3eac4f358a6233bfb

Browse Source
This commit is contained in:
ADS Merger
2020-02-11 07:08:19 +00:00
parent 0f934081e1
commit 085752f111
217 changed files with 2561 additions and 2063 deletions
Download Patch File Download Diff File Expand all files Collapse all files

67
src/vs/editor/common/config/editorOptions.ts
View File

@@ -366,6 +366,10 @@ export interface IEditorOptions {
* Defaults to 10 (ms)
*/
quickSuggestionsDelay?: number;
/**
* Controls the spacing around the editor.
*/
padding?: IEditorPaddingOptions;
/**
* Parameter hint options.
*/
@@ -2082,6 +2086,65 @@ function _multiCursorModifierFromString(multiCursorModifier: 'ctrlCmd' | 'alt'):
//#endregion
//#region padding
/**
* Configuration options for editor padding
*/
export interface IEditorPaddingOptions {
/**
* Spacing between top edge of editor and first line.
*/
top?: number;
/**
* Spacing between bottom edge of editor and last line.
*/
bottom?: number;
}
export interface InternalEditorPaddingOptions {
readonly top: number;
readonly bottom: number;
}
class EditorPadding extends BaseEditorOption<EditorOption.padding, InternalEditorPaddingOptions> {
constructor() {
super(
EditorOption.padding, 'padding', { top: 0, bottom: 0 },
{
'editor.padding.top': {
type: 'number',
default: 0,
minimum: 0,
maximum: 1000,
description: nls.localize('padding.top', "Controls the amount of space between the top edge of the editor and the first line.")
},
'editor.padding.bottom': {
type: 'number',
default: 0,
minimum: 0,
maximum: 1000,
description: nls.localize('padding.bottom', "Controls the amount of space between the bottom edge of the editor and the last line.")
}
}
);
}
public validate(_input: any): InternalEditorPaddingOptions {
if (typeof _input !== 'object') {
return this.defaultValue;
}
const input = _input as IEditorPaddingOptions;
return {
top: EditorIntOption.clampedInt(input.top, 0, 0, 1000),
bottom: EditorIntOption.clampedInt(input.bottom, 0, 0, 1000)
};
}
}
//#endregion
//#region parameterHints
/**
@@ -3188,6 +3251,7 @@ export const enum EditorOption {
occurrencesHighlight,
overviewRulerBorder,
overviewRulerLanes,
padding,
parameterHints,
peekWidgetDefaultFocus,
definitionLinkOpensInPeek,
@@ -3575,6 +3639,7 @@ export const EditorOptions = {
EditorOption.overviewRulerLanes, 'overviewRulerLanes',
3, 0, 3
)),
padding: register(new EditorPadding()),
parameterHints: register(new EditorParameterHints()),
peekWidgetDefaultFocus: register(new EditorStringEnumOption(
EditorOption.peekWidgetDefaultFocus, 'peekWidgetDefaultFocus',
@@ -3634,7 +3699,7 @@ export const EditorOptions = {
)),
renderWhitespace: register(new EditorStringEnumOption(
EditorOption.renderWhitespace, 'renderWhitespace',
'none' as 'none' | 'boundary' | 'selection' | 'all',
'selection' as 'selection' | 'none' | 'boundary' | 'all',
['none', 'boundary', 'selection', 'all'] as const,
{
enumDescriptions: [