Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
microsoft
GitHub Repository: microsoft/vscode
Path: blob/main/extensions/markdown-language-features/preview-src/scroll-sync.ts
3292 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 { SettingsManager } from './settings';
7
8
const codeLineClass = 'code-line';
9
10
11
export class CodeLineElement {
12
private readonly _detailParentElements: readonly HTMLDetailsElement[];
13
14
constructor(
15
readonly element: HTMLElement,
16
readonly line: number,
17
readonly codeElement?: HTMLElement,
18
) {
19
this._detailParentElements = Array.from(getParentsWithTagName<HTMLDetailsElement>(element, 'DETAILS'));
20
}
21
22
get isVisible(): boolean {
23
return !this._detailParentElements.some(x => !x.open);
24
}
25
}
26
27
const getCodeLineElements = (() => {
28
let cachedElements: CodeLineElement[] | undefined;
29
let cachedVersion = -1;
30
return (documentVersion: number) => {
31
if (!cachedElements || documentVersion !== cachedVersion) {
32
cachedVersion = documentVersion;
33
cachedElements = [new CodeLineElement(document.body, -1)];
34
for (const element of document.getElementsByClassName(codeLineClass)) {
35
if (!(element instanceof HTMLElement)) {
36
continue;
37
}
38
39
const line = +element.getAttribute('data-line')!;
40
if (isNaN(line)) {
41
continue;
42
}
43
44
45
if (element.tagName === 'CODE' && element.parentElement && element.parentElement.tagName === 'PRE') {
46
// Fenced code blocks are a special case since the `code-line` can only be marked on
47
// the `<code>` element and not the parent `<pre>` element.
48
cachedElements.push(new CodeLineElement(element.parentElement, line, element));
49
} else if (element.tagName === 'UL' || element.tagName === 'OL') {
50
// Skip adding list elements since the first child has the same code line (and should be preferred)
51
} else {
52
cachedElements.push(new CodeLineElement(element, line));
53
}
54
}
55
}
56
return cachedElements;
57
};
58
})();
59
60
/**
61
* Find the html elements that map to a specific target line in the editor.
62
*
63
* If an exact match, returns a single element. If the line is between elements,
64
* returns the element prior to and the element after the given line.
65
*/
66
export function getElementsForSourceLine(targetLine: number, documentVersion: number): { previous: CodeLineElement; next?: CodeLineElement } {
67
const lineNumber = Math.floor(targetLine);
68
const lines = getCodeLineElements(documentVersion);
69
let previous = lines[0] || null;
70
for (const entry of lines) {
71
if (entry.line === lineNumber) {
72
return { previous: entry, next: undefined };
73
} else if (entry.line > lineNumber) {
74
return { previous, next: entry };
75
}
76
previous = entry;
77
}
78
return { previous };
79
}
80
81
/**
82
* Find the html elements that are at a specific pixel offset on the page.
83
*/
84
export function getLineElementsAtPageOffset(offset: number, documentVersion: number): { previous: CodeLineElement; next?: CodeLineElement } {
85
const lines = getCodeLineElements(documentVersion).filter(x => x.isVisible);
86
const position = offset - window.scrollY;
87
let lo = -1;
88
let hi = lines.length - 1;
89
while (lo + 1 < hi) {
90
const mid = Math.floor((lo + hi) / 2);
91
const bounds = getElementBounds(lines[mid]);
92
if (bounds.top + bounds.height >= position) {
93
hi = mid;
94
}
95
else {
96
lo = mid;
97
}
98
}
99
const hiElement = lines[hi];
100
const hiBounds = getElementBounds(hiElement);
101
if (hi >= 1 && hiBounds.top > position) {
102
const loElement = lines[lo];
103
return { previous: loElement, next: hiElement };
104
}
105
if (hi > 1 && hi < lines.length && hiBounds.top + hiBounds.height > position) {
106
return { previous: hiElement, next: lines[hi + 1] };
107
}
108
return { previous: hiElement };
109
}
110
111
function getElementBounds({ element }: CodeLineElement): { top: number; height: number } {
112
const myBounds = element.getBoundingClientRect();
113
114
// Some code line elements may contain other code line elements.
115
// In those cases, only take the height up to that child.
116
const codeLineChild = element.querySelector(`.${codeLineClass}`);
117
if (codeLineChild) {
118
const childBounds = codeLineChild.getBoundingClientRect();
119
const height = Math.max(1, (childBounds.top - myBounds.top));
120
return {
121
top: myBounds.top,
122
height: height
123
};
124
}
125
126
return myBounds;
127
}
128
129
/**
130
* Attempt to reveal the element for a source line in the editor.
131
*/
132
export function scrollToRevealSourceLine(line: number, documentVersion: number, settingsManager: SettingsManager) {
133
if (!settingsManager.settings?.scrollPreviewWithEditor) {
134
return;
135
}
136
137
if (line <= 0) {
138
window.scroll(window.scrollX, 0);
139
return;
140
}
141
142
const { previous, next } = getElementsForSourceLine(line, documentVersion);
143
if (!previous) {
144
return;
145
}
146
let scrollTo = 0;
147
const rect = getElementBounds(previous);
148
const previousTop = rect.top;
149
if (next && next.line !== previous.line) {
150
// Between two elements. Go to percentage offset between them.
151
const betweenProgress = (line - previous.line) / (next.line - previous.line);
152
const previousEnd = previousTop + rect.height;
153
const betweenHeight = next.element.getBoundingClientRect().top - previousEnd;
154
scrollTo = previousEnd + betweenProgress * betweenHeight;
155
} else {
156
const progressInElement = line - Math.floor(line);
157
scrollTo = previousTop + (rect.height * progressInElement);
158
}
159
window.scroll(window.scrollX, Math.max(1, window.scrollY + scrollTo));
160
}
161
162
export function getEditorLineNumberForPageOffset(offset: number, documentVersion: number): number | null {
163
const { previous, next } = getLineElementsAtPageOffset(offset, documentVersion);
164
if (previous) {
165
if (previous.line < 0) {
166
return 0;
167
}
168
const previousBounds = getElementBounds(previous);
169
const offsetFromPrevious = (offset - window.scrollY - previousBounds.top);
170
if (next) {
171
const progressBetweenElements = offsetFromPrevious / (getElementBounds(next).top - previousBounds.top);
172
return previous.line + progressBetweenElements * (next.line - previous.line);
173
} else {
174
const progressWithinElement = offsetFromPrevious / (previousBounds.height);
175
return previous.line + progressWithinElement;
176
}
177
}
178
return null;
179
}
180
181
/**
182
* Try to find the html element by using a fragment id
183
*/
184
export function getLineElementForFragment(fragment: string, documentVersion: number): CodeLineElement | undefined {
185
return getCodeLineElements(documentVersion).find((element) => {
186
return element.element.id === fragment;
187
});
188
}
189
190
function* getParentsWithTagName<T extends HTMLElement>(element: HTMLElement, tagName: string): Iterable<T> {
191
for (let parent = element.parentElement; parent; parent = parent.parentElement) {
192
if (parent.tagName === tagName) {
193
yield parent as T;
194
}
195
}
196
}
197
198