Skip to content

Commit

Permalink
sphinx-agent: Update webview.js
Browse files Browse the repository at this point in the history
This aligns the `webview.js` file injected into HTML to the updated
source location information to add support for mutliple source files.
  • Loading branch information
alcarney committed Jul 11, 2024
1 parent 9fadad5 commit 2fb0b46
Showing 1 changed file with 118 additions and 52 deletions.
170 changes: 118 additions & 52 deletions lib/esbonio/esbonio/sphinx_agent/static/webview.js
Original file line number Diff line number Diff line change
@@ -1,45 +1,116 @@
// This file gets injected into html pages built with Sphinx
// which allows the webpage to talk with the preview server and coordinate details such as refreshes
// and page scrolling.
function indexScrollTargets() {
let targets = new Map()
for (let target of Array.from(document.querySelectorAll(".linemarker"))) {

let linum
for (let cls of target.classList) {
let result = cls.match(/linemarker-(\d+)/)
if (result) {
linum = parseInt(result[1])
targets.set(linum, target)
break
}

/**
* Find the uri and line number the editor should scroll to
*
* @returns {[string, number]} - The uri and line number
*/
function findEditorScrollTarget() {
const markers = document.querySelectorAll(".esbonio-marker")

for (let marker of markers) {
const bbox = marker.getBoundingClientRect()
// TODO: This probably needs to be made smarter as it does not account
// for elements that are technically on screen but hidden. - e.g. by furo's header bar.
if (bbox.top < 60) {
continue
}

const match = marker.className.match(/.* esbonio-marker-(\d+).*/)
if (!match || !match[1]) {
console.debug(`Unable to find marker id in '${marker.className}'`)
return
}

const markerId = match[1]
const location = document.querySelector(`#esbonio-marker-index span[data-id="${markerId}"]`)
if (!location) {
console.debug(`Unable to locate source for marker id: '${markerId}'`)
return
}

const uri = location.dataset.uri
const line = parseInt(location.dataset.line)
return [uri, line]
}

return targets
return
}

// Return the line number we should ask the editor to scroll to.
function findScrollTarget() {
/**
* Scroll the webview to show the given location
*
* @param {string} uri - The uri of the document to reveal
* @param {number} linum - The line number within that document to reveal
*/
function scrollViewTo(uri, linum) {

// Select all the markers with the given uri.
const markers = Array.from(
document.querySelectorAll(`#esbonio-marker-index span[data-uri="${uri}"]`)
)

// Are we at the top of the page?
if (window.scrollY <= 100) {
return -1
if (!markers) {
return
}

for (let [linum, target] of scrollTargets.entries()) {
const bbox = target.getBoundingClientRect()
// TODO: This probably needs to be made smarter as it does not account
// for elements that are technically on screen but hidden. - e.g. by furo's header bar.
if (bbox.top > 0) {
return linum
/** @type {HTMLElement} */
let current

/** @type {number} */
let currentLine = 0

/** @type {HTMLElement} */
let previous

/** @type {number} */
let previousLine

for (let marker of markers) {
let markerId = marker.dataset.id
let markerLine = parseInt(marker.dataset.line)
let element = document.querySelector(`.esbonio-marker-${markerId}`)

// Only consider markers that correspond with an element currently in the DOM
if (!element) {
continue
}

current = element
currentLine = markerLine

// Have we passed the target line number?
if (markerLine > linum) {
break
}

previous = current
previousLine = currentLine
}

return
}
if (!current) {
return
}

if (!previous) {
previous = current
previousLine = currentLine
}

// Scroll the view to a position that is an interpolation between the previous and
// current marker based on the requested line number.
const previousPos = window.scrollY + previous.getBoundingClientRect().top
const currentPos = window.scrollY + current.getBoundingClientRect().top

let scrollTargets = new Map()
const t = (linum - previousLine) / Math.max(currentLine - previousLine, 1)
const y = (1 - t) * previousPos + t * currentPos

console.table({line: linum, previous: previousLine, current: currentLine, t: t, y: y})

window.scrollTo(0, y - 60)
}

const host = window.location.hostname;
const queryString = window.location.search;
Expand Down Expand Up @@ -67,20 +138,7 @@ const handlers = {
console.debug("Reloading page...")
window.location.reload()
},
"view/scroll": function (params) {
if (params.line <= 1) {
window.scrollTo(0, 0)
return
}

// TODO: Look for targets within X of target line instead?
let target = scrollTargets.get(params.line)
if (!target) {
return
}

target.scrollIntoView(true)
}
"view/scroll": (params) => {scrollViewTo(params.uri, params.line)}
}

function handle(message) {
Expand All @@ -91,14 +149,15 @@ function handle(message) {
console.error(`Error: ${JSON.stringify(message.error, undefined, 2)}`)
} else if (message.method) {
let method = message.method
console.debug(`Got request: ${method}, ${JSON.stringify(params, undefined, 2)}`)
console.debug(`Request: ${method}, ${JSON.stringify(params, undefined, 2)}`)
} else {
let result = message.result
console.debug(`Got response: ${JSON.stringify(result, undefined, 2)}`)
console.debug(`Response: ${JSON.stringify(result, undefined, 2)}`)
}
} else {
let handler = handlers[message.method]
if (handler) {
// console.debug(`Notification: ${message.method}, ${JSON.stringify(message.params)} `)
handler(message.params)
} else {
console.error(`Got unknown notification: '${message.method}'`)
Expand All @@ -107,13 +166,23 @@ function handle(message) {
}

window.addEventListener("scroll", (event) => {
let linum = findScrollTarget()
if (linum) {
// TODO: Rate limits.
sendMessage(
{ jsonrpc: "2.0", method: "editor/scroll", params: { line: linum } }
)
const target = findEditorScrollTarget()
if (!target) {
return
}

const uri = target[0]
const line = target[1]

if (!uri || !line) {
return
}

// TODO: Rate limits.
sendMessage(
{ jsonrpc: "2.0", method: "editor/scroll", params: { uri: uri, line: line } }
)

})

// Connection opened
Expand All @@ -128,9 +197,6 @@ socket.addEventListener("message", (event) => {
});

function main() {
scrollTargets = indexScrollTargets()
console.debug(scrollTargets)

if (showMarkers) {
let markerStyle = document.createElement('style')
let lines = [".linemarker { background: rgb(255, 0, 0, 0.25); position: relative; }"]
Expand Down

0 comments on commit 2fb0b46

Please sign in to comment.