diff --git a/services/web/frontend/js/ide/editor/EditorManager.js b/services/web/frontend/js/ide/editor/EditorManager.js index 8efc0f644c..1cd19e8e45 100644 --- a/services/web/frontend/js/ide/editor/EditorManager.js +++ b/services/web/frontend/js/ide/editor/EditorManager.js @@ -128,7 +128,8 @@ export default (EditorManager = (function() { return this.$scope.$broadcast( 'editor:gotoLine', options.gotoLine, - options.gotoColumn + options.gotoColumn, + options.syncToPdf ) } diff --git a/services/web/frontend/js/ide/editor/directives/aceEditor/cursor-position/CursorPositionManager.js b/services/web/frontend/js/ide/editor/directives/aceEditor/cursor-position/CursorPositionManager.js index e7cbce9503..f6aca22206 100644 --- a/services/web/frontend/js/ide/editor/directives/aceEditor/cursor-position/CursorPositionManager.js +++ b/services/web/frontend/js/ide/editor/directives/aceEditor/cursor-position/CursorPositionManager.js @@ -30,13 +30,17 @@ export default (CursorPositionManager = class CursorPositionManager { this.$scope.$on('changeEditor', this.storePositionAndLine) - this.$scope.$on(`${this.$scope.name}:gotoLine`, (e, line, column) => { - if (line != null) { - return setTimeout(() => { - return this.adapter.gotoLine(line, column) - }, 10) + this.$scope.$on( + `${this.$scope.name}:gotoLine`, + (e, line, column, syncToPdf) => { + if (line != null) { + return setTimeout(() => { + this.adapter.gotoLine(line, column) + if (syncToPdf) this.onSyncToPdf() + }, 10) + } } - }) // Hack: Must happen after @gotoStoredPosition + ) // Hack: Must happen after @gotoStoredPosition this.$scope.$on(`${this.$scope.name}:gotoOffset`, (e, offset) => { if (offset != null) { diff --git a/services/web/frontend/js/ide/outline/OutlineManager.js b/services/web/frontend/js/ide/outline/OutlineManager.js index 440bcd192b..9b67ae0a7e 100644 --- a/services/web/frontend/js/ide/outline/OutlineManager.js +++ b/services/web/frontend/js/ide/outline/OutlineManager.js @@ -94,9 +94,9 @@ class OutlineManager { this.broadcastChangeEvent() } - jumpToLine(line) { + jumpToLine(line, syncToPdf) { this.ignoreNextScroll = true - this.ide.editorManager.jumpToLine({ gotoLine: line }) + this.ide.editorManager.jumpToLine({ gotoLine: line, syncToPdf }) } broadcastChangeEvent() { diff --git a/services/web/frontend/js/ide/outline/components/OutlineItem.js b/services/web/frontend/js/ide/outline/components/OutlineItem.js index 48548bb70d..33823bee3e 100644 --- a/services/web/frontend/js/ide/outline/components/OutlineItem.js +++ b/services/web/frontend/js/ide/outline/components/OutlineItem.js @@ -1,5 +1,6 @@ import React, { useState, useEffect, createRef, useRef } from 'react' import PropTypes from 'prop-types' +import scrollIntoViewIfNeeded from 'scroll-into-view-if-needed' import classNames from 'classnames' import OutlineList from './OutlineList' @@ -39,7 +40,11 @@ function OutlineItem({ outlineItem, jumpToLine, highlightedLine }) { } function handleOutlineItemLinkClick() { - jumpToLine(outlineItem.line) + jumpToLine(outlineItem.line, false) + } + + function handleOutlineItemLinkDoubleClick() { + jumpToLine(outlineItem.line, true) } useEffect( @@ -50,7 +55,8 @@ function OutlineItem({ outlineItem, jumpToLine, highlightedLine }) { isHighlightedRef.current = isNowHighlighted if (!wasHighlighted && isNowHighlighted) { - titleElementRef.current.scrollIntoView({ + scrollIntoViewIfNeeded(titleElementRef.current, { + scrollMode: 'if-needed', block: 'center' }) } @@ -72,6 +78,7 @@ function OutlineItem({ outlineItem, jumpToLine, highlightedLine }) {