Extract line number gutter width calculation and improve text selection
This commit is contained in:
@@ -1,3 +1,12 @@
|
||||
/**
|
||||
* Compute the pixel width for a line-number gutter based on the highest
|
||||
* line number that will be displayed. Minimum width accommodates 2 digits.
|
||||
*/
|
||||
export function lineNumberGutterWidth(maxLineNumber: number): number {
|
||||
const digits = Math.max(2, String(maxLineNumber).length);
|
||||
return digits * 8 + 12;
|
||||
}
|
||||
|
||||
export function getCodeInsets(theme: any) {
|
||||
const padding =
|
||||
typeof theme.spacing?.[3] === "number"
|
||||
|
||||
Reference in New Issue
Block a user