2020-06-06 17:00:20 +02:00
|
|
|
// Helper functions to sync up scrolling
|
|
|
|
export default function useScrollUtils(CodeMirror: any) {
|
|
|
|
function getScrollHeight(cm: any) {
|
|
|
|
const info = cm.getScrollInfo();
|
|
|
|
const overdraw = cm.state.scrollPastEndPadding ? cm.state.scrollPastEndPadding : '0px';
|
2020-08-04 23:36:50 +02:00
|
|
|
return info.height - info.clientHeight - parseInt(overdraw, 10);
|
2020-06-06 17:00:20 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
CodeMirror.defineExtension('getScrollPercent', function() {
|
|
|
|
const info = this.getScrollInfo();
|
|
|
|
|
|
|
|
return info.top / getScrollHeight(this);
|
|
|
|
});
|
|
|
|
|
|
|
|
CodeMirror.defineExtension('setScrollPercent', function(p: number) {
|
|
|
|
this.scrollTo(null, p * getScrollHeight(this));
|
|
|
|
});
|
|
|
|
|
|
|
|
}
|