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