Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
microsoft
GitHub Repository: microsoft/vscode
Path: blob/main/src/vs/editor/common/config/fontInfo.ts
3295 views
1
/*---------------------------------------------------------------------------------------------
2
* Copyright (c) Microsoft Corporation. All rights reserved.
3
* Licensed under the MIT License. See License.txt in the project root for license information.
4
*--------------------------------------------------------------------------------------------*/
5
6
import * as platform from '../../../base/common/platform.js';
7
import { EditorFontVariations, EditorOptions, EditorOption, FindComputedEditorOptionValueById, EDITOR_FONT_DEFAULTS } from './editorOptions.js';
8
import { EditorZoom } from './editorZoom.js';
9
10
/**
11
* Determined from empirical observations.
12
* @internal
13
*/
14
export const GOLDEN_LINE_HEIGHT_RATIO = platform.isMacintosh ? 1.5 : 1.35;
15
16
/**
17
* @internal
18
*/
19
export const MINIMUM_LINE_HEIGHT = 8;
20
21
/**
22
* @internal
23
*/
24
export interface IValidatedEditorOptions {
25
get<T extends EditorOption>(id: T): FindComputedEditorOptionValueById<T>;
26
}
27
28
export class BareFontInfo {
29
readonly _bareFontInfoBrand: void = undefined;
30
31
/**
32
* @internal
33
*/
34
public static createFromValidatedSettings(options: IValidatedEditorOptions, pixelRatio: number, ignoreEditorZoom: boolean): BareFontInfo {
35
const fontFamily = options.get(EditorOption.fontFamily);
36
const fontWeight = options.get(EditorOption.fontWeight);
37
const fontSize = options.get(EditorOption.fontSize);
38
const fontFeatureSettings = options.get(EditorOption.fontLigatures);
39
const fontVariationSettings = options.get(EditorOption.fontVariations);
40
const lineHeight = options.get(EditorOption.lineHeight);
41
const letterSpacing = options.get(EditorOption.letterSpacing);
42
return BareFontInfo._create(fontFamily, fontWeight, fontSize, fontFeatureSettings, fontVariationSettings, lineHeight, letterSpacing, pixelRatio, ignoreEditorZoom);
43
}
44
45
/**
46
* @internal
47
*/
48
public static createFromRawSettings(opts: { fontFamily?: string; fontWeight?: string; fontSize?: number; fontLigatures?: boolean | string; fontVariations?: boolean | string; lineHeight?: number; letterSpacing?: number }, pixelRatio: number, ignoreEditorZoom: boolean = false): BareFontInfo {
49
const fontFamily = EditorOptions.fontFamily.validate(opts.fontFamily);
50
const fontWeight = EditorOptions.fontWeight.validate(opts.fontWeight);
51
const fontSize = EditorOptions.fontSize.validate(opts.fontSize);
52
const fontFeatureSettings = EditorOptions.fontLigatures2.validate(opts.fontLigatures);
53
const fontVariationSettings = EditorOptions.fontVariations.validate(opts.fontVariations);
54
const lineHeight = EditorOptions.lineHeight.validate(opts.lineHeight);
55
const letterSpacing = EditorOptions.letterSpacing.validate(opts.letterSpacing);
56
return BareFontInfo._create(fontFamily, fontWeight, fontSize, fontFeatureSettings, fontVariationSettings, lineHeight, letterSpacing, pixelRatio, ignoreEditorZoom);
57
}
58
59
/**
60
* @internal
61
*/
62
private static _create(fontFamily: string, fontWeight: string, fontSize: number, fontFeatureSettings: string, fontVariationSettings: string, lineHeight: number, letterSpacing: number, pixelRatio: number, ignoreEditorZoom: boolean): BareFontInfo {
63
if (lineHeight === 0) {
64
lineHeight = GOLDEN_LINE_HEIGHT_RATIO * fontSize;
65
} else if (lineHeight < MINIMUM_LINE_HEIGHT) {
66
// Values too small to be line heights in pixels are in ems.
67
lineHeight = lineHeight * fontSize;
68
}
69
70
// Enforce integer, minimum constraints
71
lineHeight = Math.round(lineHeight);
72
if (lineHeight < MINIMUM_LINE_HEIGHT) {
73
lineHeight = MINIMUM_LINE_HEIGHT;
74
}
75
76
const editorZoomLevelMultiplier = 1 + (ignoreEditorZoom ? 0 : EditorZoom.getZoomLevel() * 0.1);
77
fontSize *= editorZoomLevelMultiplier;
78
lineHeight *= editorZoomLevelMultiplier;
79
80
if (fontVariationSettings === EditorFontVariations.TRANSLATE) {
81
if (fontWeight === 'normal' || fontWeight === 'bold') {
82
fontVariationSettings = EditorFontVariations.OFF;
83
} else {
84
const fontWeightAsNumber = parseInt(fontWeight, 10);
85
fontVariationSettings = `'wght' ${fontWeightAsNumber}`;
86
fontWeight = 'normal';
87
}
88
}
89
90
return new BareFontInfo({
91
pixelRatio: pixelRatio,
92
fontFamily: fontFamily,
93
fontWeight: fontWeight,
94
fontSize: fontSize,
95
fontFeatureSettings: fontFeatureSettings,
96
fontVariationSettings,
97
lineHeight: lineHeight,
98
letterSpacing: letterSpacing
99
});
100
}
101
102
readonly pixelRatio: number;
103
readonly fontFamily: string;
104
readonly fontWeight: string;
105
readonly fontSize: number;
106
readonly fontFeatureSettings: string;
107
readonly fontVariationSettings: string;
108
readonly lineHeight: number;
109
readonly letterSpacing: number;
110
111
/**
112
* @internal
113
*/
114
protected constructor(opts: {
115
pixelRatio: number;
116
fontFamily: string;
117
fontWeight: string;
118
fontSize: number;
119
fontFeatureSettings: string;
120
fontVariationSettings: string;
121
lineHeight: number;
122
letterSpacing: number;
123
}) {
124
this.pixelRatio = opts.pixelRatio;
125
this.fontFamily = String(opts.fontFamily);
126
this.fontWeight = String(opts.fontWeight);
127
this.fontSize = opts.fontSize;
128
this.fontFeatureSettings = opts.fontFeatureSettings;
129
this.fontVariationSettings = opts.fontVariationSettings;
130
this.lineHeight = opts.lineHeight | 0;
131
this.letterSpacing = opts.letterSpacing;
132
}
133
134
/**
135
* @internal
136
*/
137
public getId(): string {
138
return `${this.pixelRatio}-${this.fontFamily}-${this.fontWeight}-${this.fontSize}-${this.fontFeatureSettings}-${this.fontVariationSettings}-${this.lineHeight}-${this.letterSpacing}`;
139
}
140
141
/**
142
* @internal
143
*/
144
public getMassagedFontFamily(): string {
145
const fallbackFontFamily = EDITOR_FONT_DEFAULTS.fontFamily;
146
const fontFamily = BareFontInfo._wrapInQuotes(this.fontFamily);
147
if (fallbackFontFamily && this.fontFamily !== fallbackFontFamily) {
148
return `${fontFamily}, ${fallbackFontFamily}`;
149
}
150
return fontFamily;
151
}
152
153
private static _wrapInQuotes(fontFamily: string): string {
154
if (/[,"']/.test(fontFamily)) {
155
// Looks like the font family might be already escaped
156
return fontFamily;
157
}
158
if (/[+ ]/.test(fontFamily)) {
159
// Wrap a font family using + or <space> with quotes
160
return `"${fontFamily}"`;
161
}
162
return fontFamily;
163
}
164
}
165
166
// change this whenever `FontInfo` members are changed
167
export const SERIALIZED_FONT_INFO_VERSION = 2;
168
169
export class FontInfo extends BareFontInfo {
170
readonly _editorStylingBrand: void = undefined;
171
172
readonly version: number = SERIALIZED_FONT_INFO_VERSION;
173
readonly isTrusted: boolean;
174
readonly isMonospace: boolean;
175
readonly typicalHalfwidthCharacterWidth: number;
176
readonly typicalFullwidthCharacterWidth: number;
177
readonly canUseHalfwidthRightwardsArrow: boolean;
178
readonly spaceWidth: number;
179
readonly middotWidth: number;
180
readonly wsmiddotWidth: number;
181
readonly maxDigitWidth: number;
182
183
/**
184
* @internal
185
*/
186
constructor(opts: {
187
pixelRatio: number;
188
fontFamily: string;
189
fontWeight: string;
190
fontSize: number;
191
fontFeatureSettings: string;
192
fontVariationSettings: string;
193
lineHeight: number;
194
letterSpacing: number;
195
isMonospace: boolean;
196
typicalHalfwidthCharacterWidth: number;
197
typicalFullwidthCharacterWidth: number;
198
canUseHalfwidthRightwardsArrow: boolean;
199
spaceWidth: number;
200
middotWidth: number;
201
wsmiddotWidth: number;
202
maxDigitWidth: number;
203
}, isTrusted: boolean) {
204
super(opts);
205
this.isTrusted = isTrusted;
206
this.isMonospace = opts.isMonospace;
207
this.typicalHalfwidthCharacterWidth = opts.typicalHalfwidthCharacterWidth;
208
this.typicalFullwidthCharacterWidth = opts.typicalFullwidthCharacterWidth;
209
this.canUseHalfwidthRightwardsArrow = opts.canUseHalfwidthRightwardsArrow;
210
this.spaceWidth = opts.spaceWidth;
211
this.middotWidth = opts.middotWidth;
212
this.wsmiddotWidth = opts.wsmiddotWidth;
213
this.maxDigitWidth = opts.maxDigitWidth;
214
}
215
216
/**
217
* @internal
218
*/
219
public equals(other: FontInfo): boolean {
220
return (
221
this.fontFamily === other.fontFamily
222
&& this.fontWeight === other.fontWeight
223
&& this.fontSize === other.fontSize
224
&& this.fontFeatureSettings === other.fontFeatureSettings
225
&& this.fontVariationSettings === other.fontVariationSettings
226
&& this.lineHeight === other.lineHeight
227
&& this.letterSpacing === other.letterSpacing
228
&& this.typicalHalfwidthCharacterWidth === other.typicalHalfwidthCharacterWidth
229
&& this.typicalFullwidthCharacterWidth === other.typicalFullwidthCharacterWidth
230
&& this.canUseHalfwidthRightwardsArrow === other.canUseHalfwidthRightwardsArrow
231
&& this.spaceWidth === other.spaceWidth
232
&& this.middotWidth === other.middotWidth
233
&& this.wsmiddotWidth === other.wsmiddotWidth
234
&& this.maxDigitWidth === other.maxDigitWidth
235
);
236
}
237
}
238
239