ckaczor/azuredatastudio
1
0
Fork 0
mirror of https://github.com/ckaczor/azuredatastudio.git synced 2026-01-24 17:23:05 -05:00
Code Issues Packages Projects Releases Wiki Activity

Merge from vscode a5cf1da01d5db3d2557132be8d30f89c38019f6c (#8525)

Browse Source 
* Merge from vscode a5cf1da01d5db3d2557132be8d30f89c38019f6c

* remove files we don't want

* fix hygiene

* update distro

* update distro

* fix hygiene

* fix strict nulls

* distro

* distro

* fix tests

* fix tests

* add another edit

* fix viewlet icon

* fix azure dialog

* fix some padding

* fix more padding issues
This commit is contained in:
Anthony Dresser
2019-12-04 19:28:22 -08:00
committed by GitHub
parent a8818ab0df
commit f5ce7fb2a5
1507 changed files with 42813 additions and 27370 deletions
Download Patch File Download Diff File Expand all files Collapse all files

47
extensions/markdown-language-features/preview-src/scroll-sync.ts
View File

@@ -5,6 +5,7 @@
import { getSettings } from './settings';
const codeLineClass = 'code-line';
function clamp(min: number, max: number, value: number) {
return Math.min(max, Math.max(min, value));
@@ -25,9 +26,17 @@ const getCodeLineElements = (() => {
return () => {
if (!elements) {
elements = [{ element: document.body, line: 0 }];
for (const element of document.getElementsByClassName('code-line')) {
for (const element of document.getElementsByClassName(codeLineClass)) {
const line = +element.getAttribute('data-line')!;
if (!isNaN(line)) {
if (isNaN(line)) {
continue;
}
if (element.tagName === 'CODE' && element.parentElement && element.parentElement.tagName === 'PRE') {
// Fenched code blocks are a special case since the `code-line` can only be marked on
// the `<code>` element and not the parent `<pre>` element.
elements.push({ element: element.parentElement as HTMLElement, line });
} else {
elements.push({ element: element as HTMLElement, line });
}
}
@@ -67,7 +76,7 @@ export function getLineElementsAtPageOffset(offset: number): { previous: CodeLin
let hi = lines.length - 1;
while (lo + 1 < hi) {
const mid = Math.floor((lo + hi) / 2);
const bounds = lines[mid].element.getBoundingClientRect();
const bounds = getElementBounds(lines[mid]);
if (bounds.top + bounds.height >= position) {
hi = mid;
}
@@ -76,14 +85,35 @@ export function getLineElementsAtPageOffset(offset: number): { previous: CodeLin
}
}
const hiElement = lines[hi];
const hiBounds = hiElement.element.getBoundingClientRect();
const hiBounds = getElementBounds(hiElement);
if (hi >= 1 && hiBounds.top > position) {
const loElement = lines[lo];
return { previous: loElement, next: hiElement };
}
if (hi > 1 && hi < lines.length && hiBounds.top + hiBounds.height > position) {
return { previous: hiElement, next: lines[hi + 1] };
}
return { previous: hiElement };
}
function getElementBounds({ element }: CodeLineElement): { top: number, height: number } {
const myBounds = element.getBoundingClientRect();
// Some code line elements may contain other code line elements.
// In those cases, only take the height up to that child.
const codeLineChild = element.querySelector(`.${codeLineClass}`);
if (codeLineChild) {
const childBounds = codeLineChild.getBoundingClientRect();
const height = Math.max(1, (childBounds.top - myBounds.top));
return {
top: myBounds.top,
height: height
};
}
return myBounds;
}
/**
* Attempt to reveal the element for a source line in the editor.
*/
@@ -102,7 +132,7 @@ export function scrollToRevealSourceLine(line: number) {
return;
}
let scrollTo = 0;
const rect = previous.element.getBoundingClientRect();
const rect = getElementBounds(previous);
const previousTop = rect.top;
if (next && next.line !== previous.line) {
// Between two elements. Go to percentage offset between them.
@@ -119,14 +149,13 @@ export function scrollToRevealSourceLine(line: number) {
export function getEditorLineNumberForPageOffset(offset: number) {
const { previous, next } = getLineElementsAtPageOffset(offset);
if (previous) {
const previousBounds = previous.element.getBoundingClientRect();
const previousBounds = getElementBounds(previous);
const offsetFromPrevious = (offset - window.scrollY - previousBounds.top);
if (next) {
const progressBetweenElements = offsetFromPrevious / (next.element.getBoundingClientRect().top - previousBounds.top);
const progressBetweenElements = offsetFromPrevious / (getElementBounds(next).top - previousBounds.top);
const line = previous.line + progressBetweenElements * (next.line - previous.line);
return clampLine(line);
}
else {
} else {
const progressWithinElement = offsetFromPrevious / (previousBounds.height);
const line = previous.line + progressWithinElement;
return clampLine(line);