diff --git a/static/index.ts b/static/index.ts index 75175c944..0e5b4f5eb 100644 --- a/static/index.ts +++ b/static/index.ts @@ -86,7 +86,6 @@ type HsMsg = { const orderedCells : Cell[] = [] const cells = new Map() -const curHighlights : Div[] = [] // HTML elements currently highlighted function processUpdates(msg:HsMsg) { dropCells(msg.orderedNodesUpdate.numDropped) @@ -177,54 +176,25 @@ function updateCellContents(cell:Cell, update:HsCellUpdate) { setCellStatus(cell, statusUpdate["contents"])} extendCellOutput(cell, outputs) } -function removeHover() { - hoverInfoDiv.innerHTML = "" - curHighlights.map(function (element) { - element.classList.remove("highlight-group", "highlight-leaf", "status-hover")}) - curHighlights.length = 0 -} function attachStatusHovertip(cell:Cell) { - cell.status.addEventListener("mouseover", function (event:Event) { - event.stopPropagation() - cell.status.classList.add("status-hover") - curHighlights.push(cell.status) - setHoverInfo(cell.sourceText)}) - cell.status.addEventListener("mouseout", function (event:Event) { - event.stopPropagation() - removeHover()}) + addHoverAction(cell.status , () => applyHoverStatus(cell)) + if (cell.curStatus !== "Inert") { + addHoverAction(cell.lineNums, () => applyHoverStatus(cell)) + } +} +function applyHoverStatus(cell:Cell) { + addHoverClass(cell.status , "status-hover") + addHoverClass(cell.lineNums, "status-hover") } function attachHovertip(cell:Cell, srcId:SrcId) { let span = selectSpan(cell, srcId) if (span !== null) { - span.addEventListener("mouseover", function (event:Event) { - event.stopPropagation() - applyCellHover(cell, srcId)}) - span.addEventListener("mouseout" , function (event:Event) { - event.stopPropagation() - removeHover()})} -} -function addChild(div:Div, className:string) : Div { - const child = document.createElement("div") - child.className = className - div.appendChild(child) - return child -} -function appendText(div:Div, s:string) { - div.appendChild(document.createTextNode(s)) + addHoverAction(span, ()=>applyCellHover(cell, srcId))} } function selectSpan(cell:Cell, srcId:SrcId) : Div | null { const spanId : string = "#span_".concat(cell.cellId.toString(), "_", srcId.toString()) return cell.source.querySelector(spanId) } -function spansBetween(l:Div, r:Div) : Div[] { - let spans : Div[] = [] - let curL : Div | null = l - while (curL !== null && !(Object.is(curL, r))) { - spans.push(curL); - curL = curL.nextElementSibling;} - spans.push(r) - return spans -} function cellStatusClass(status: Status) : string { switch (status) { case "Waiting": @@ -364,8 +334,11 @@ function highlightTreeNode(isTemporary: boolean, node: TreeNode, highlightType:H let [l, r] = node.span let spans = spansBetween(l, r) spans.map(function (span) { - span.classList.add(highlightClass) - if (isTemporary) {curHighlights.push(span)}})} + if (isTemporary) { + addHoverClass(span, highlightClass) + } else { + span.classList.add(highlightClass) + }})} } type RenderMode = "Static" | "Dynamic" function render(renderMode:RenderMode) { @@ -411,3 +384,47 @@ function renderLaTeX(root:Div) { // renderMathInElement(proseBlock, katexOptions) // ); } + +// === hover system === + +const curHighlights : [Div, string][] = [] // HTML elements currently highlighted +function addHoverClass(div: Div, className: string) { + div.classList.add(className) + curHighlights.push([div, className]) +} +function addHoverAction(div: Div, handler:()=>void) { + div.addEventListener( "mouseover", (event:Event) => { + event.stopPropagation() + handler()}) + div.addEventListener("mouseout", function (event:Event) { + event.stopPropagation() + removeHover()}) +} +function removeHover() { + hoverInfoDiv.innerHTML = "" + curHighlights.map(function (elementAndClass:[Div, string]) { + const [element, className] = elementAndClass + element.classList.remove(className)}) + curHighlights.length = 0 +} + +// === utils === + +function spansBetween(l:Div, r:Div) : Div[] { + let spans : Div[] = [] + let curL : Div | null = l + while (curL !== null && !(Object.is(curL, r))) { + spans.push(curL); + curL = curL.nextElementSibling;} + spans.push(r) + return spans +} +function addChild(div:Div, className:string) : Div { + const child = document.createElement("div") + child.className = className + div.appendChild(child) + return child +} +function appendText(div:Div, s:string) { + div.appendChild(document.createTextNode(s)) +}