Adjust editor config (#976)

* Adjust editor config

Signed-off-by: Tilman Vatteroth <tilman.vatteroth@tu-dortmund.de>
Co-authored-by: Erik Michelson <github@erik.michelson.eu>
This commit is contained in:
Tilman Vatteroth 2021-02-03 22:13:04 +01:00 committed by GitHub
parent 0180c75e55
commit e12dc523f8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
301 changed files with 4393 additions and 3741 deletions

View file

@ -11,10 +11,10 @@ import { useOnUserScroll } from './use-on-user-scroll'
import { useScrollToLineMark } from './use-scroll-to-line-mark'
export const useSyncedScrolling = (outerContainerRef: React.RefObject<HTMLElement>,
rendererRef: React.RefObject<HTMLElement>,
numberOfLines: number,
scrollState?: ScrollState,
onScroll?: (scrollState: ScrollState) => void): [(lineMarkers: LineMarkerPosition[]) => void, () => void] => {
rendererRef: React.RefObject<HTMLElement>,
numberOfLines: number,
scrollState?: ScrollState,
onScroll?: (scrollState: ScrollState) => void): [(lineMarkers: LineMarkerPosition[]) => void, () => void] => {
const [lineMarks, setLineMarks] = useState<LineMarkerPosition[]>()
const onLineMarkerPositionChanged = useCallback((linkMarkerPositions: LineMarkerPosition[]) => {