[visual] Add coordsAt to decoration widgets (#19577)

GitOrigin-RevId: d445e68a14bbe819e126b6bf6a2328a00520c39a
This commit is contained in:
Alf Eaton 2024-07-29 13:30:48 +01:00 committed by Copybot
parent 8821a6d2f4
commit e4d971151b
27 changed files with 108 additions and 0 deletions

View file

@ -33,6 +33,10 @@ export class BeginTheoremWidget extends BeginWidget {
) )
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
buildName(nameElement: HTMLSpanElement, view: EditorView) { buildName(nameElement: HTMLSpanElement, view: EditorView) {
nameElement.textContent = this.name nameElement.textContent = this.name
if (this.argumentNode) { if (this.argumentNode) {

View file

@ -41,6 +41,10 @@ export class BeginWidget extends WidgetType {
return event.type !== 'mouseup' return event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
buildName(name: HTMLSpanElement, view: EditorView) { buildName(name: HTMLSpanElement, view: EditorView) {
name.textContent = this.environment name.textContent = this.environment
} }

View file

@ -21,4 +21,8 @@ export class BraceWidget extends WidgetType {
eq(widget: BraceWidget) { eq(widget: BraceWidget) {
return widget.content === this.content return widget.content === this.content
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -24,6 +24,10 @@ export class CharacterWidget extends WidgetType {
ignoreEvent(event: Event) { ignoreEvent(event: Event) {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }
export const COMMAND_SUBSTITUTIONS = new Map([ export const COMMAND_SUBSTITUTIONS = new Map([

View file

@ -25,6 +25,10 @@ export class DescriptionItemWidget extends WidgetType {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
setProperties(element: HTMLElement) { setProperties(element: HTMLElement) {
element.style.setProperty('--list-depth', String(this.listDepth)) element.style.setProperty('--list-depth', String(this.listDepth))
} }

View file

@ -14,4 +14,8 @@ export class DividerWidget extends WidgetType {
updateDOM(): boolean { updateDOM(): boolean {
return true return true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -41,6 +41,10 @@ export class EditableGraphicsWidget extends GraphicsWidget {
return true return true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
createEditButton(view: EditorView) { createEditButton(view: EditorView) {
const button = document.createElement('button') const button = document.createElement('button')
button.setAttribute('aria-label', view.state.phrase('edit_figure')) button.setAttribute('aria-label', view.state.phrase('edit_figure'))

View file

@ -40,6 +40,10 @@ export class EditableInlineGraphicsWidget extends EditableGraphicsWidget {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
// We set the actual figure width on the span rather than the img element // We set the actual figure width on the span rather than the img element
getFigureWidth(): string { getFigureWidth(): string {
return '100%' return '100%'

View file

@ -21,6 +21,10 @@ export class EndDocumentWidget extends WidgetType {
return true return true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
get estimatedHeight() { get estimatedHeight() {
return 30 return 30
} }

View file

@ -10,4 +10,8 @@ export class EndWidget extends WidgetType {
eq(widget: EndWidget) { eq(widget: EndWidget) {
return true return true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -39,4 +39,8 @@ export class EnvironmentLineWidget extends WidgetType {
ignoreEvent(event: Event): boolean { ignoreEvent(event: Event): boolean {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -32,4 +32,8 @@ export class FootnoteWidget extends WidgetType {
ignoreEvent(event: Event) { ignoreEvent(event: Event) {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -74,4 +74,8 @@ export class FrameWidget extends WidgetType {
ignoreEvent(event: Event) { ignoreEvent(event: Event) {
return event.type !== 'mouseup' return event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -74,6 +74,10 @@ export class GraphicsWidget extends WidgetType {
this.destroyed = true this.destroyed = true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
get estimatedHeight(): number { get estimatedHeight(): number {
return this.height return this.height
} }

View file

@ -27,4 +27,8 @@ export class IconBraceWidget extends WidgetType {
element.textContent = this.content ?? '' element.textContent = this.content ?? ''
return true return true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -24,4 +24,8 @@ export class IndicatorWidget extends WidgetType {
ignoreEvent(event: Event) { ignoreEvent(event: Event) {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -16,4 +16,8 @@ export class InlineGraphicsWidget extends GraphicsWidget {
ignoreEvent(event: Event) { ignoreEvent(event: Event) {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -51,6 +51,10 @@ export class ItemWidget extends WidgetType {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
setProperties(element: HTMLElement) { setProperties(element: HTMLElement) {
element.style.setProperty('--list-depth', String(this.listDepth)) element.style.setProperty('--list-depth', String(this.listDepth))
element.style.setProperty('--list-ordinal', String(this.ordinal)) element.style.setProperty('--list-ordinal', String(this.ordinal))

View file

@ -15,4 +15,8 @@ export class LaTeXWidget extends WidgetType {
ignoreEvent(event: Event) { ignoreEvent(event: Event) {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -51,6 +51,10 @@ export class MakeTitleWidget extends WidgetType {
this.destroyed = true this.destroyed = true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
buildContent(view: EditorView, element: HTMLElement) { buildContent(view: EditorView, element: HTMLElement) {
if (this.preamble.title) { if (this.preamble.title) {
const titleElement = buildTitleElement( const titleElement = buildTitleElement(

View file

@ -65,6 +65,10 @@ export class MathWidget extends WidgetType {
this.destroyed = true this.destroyed = true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
async renderMath(element: HTMLElement) { async renderMath(element: HTMLElement) {
const MathJax = await loadMathJax() const MathJax = await loadMathJax()

View file

@ -84,6 +84,10 @@ export class PreambleWidget extends WidgetType {
return this.expanded === other.expanded return this.expanded === other.expanded
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
get estimatedHeight() { get estimatedHeight() {
return this.expanded ? -1 : 54 return this.expanded ? -1 : 54
} }

View file

@ -24,6 +24,10 @@ export class SpaceWidget extends WidgetType {
ignoreEvent(event: Event) { ignoreEvent(event: Event) {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }
// https://tex.stackexchange.com/a/74354 // https://tex.stackexchange.com/a/74354

View file

@ -40,4 +40,8 @@ export class TableRenderingErrorWidget extends WidgetType {
} }
return element return element
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -59,6 +59,10 @@ export class TabularWidget extends WidgetType {
return true return true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
get estimatedHeight() { get estimatedHeight() {
return this.parsedTableData.table.rows.length * 50 return this.parsedTableData.table.rows.length * 50
} }

View file

@ -15,4 +15,8 @@ export class TeXWidget extends WidgetType {
ignoreEvent(event: Event) { ignoreEvent(event: Event) {
return event.type !== 'mousedown' && event.type !== 'mouseup' return event.type !== 'mousedown' && event.type !== 'mouseup'
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }

View file

@ -10,4 +10,8 @@ export class TildeWidget extends WidgetType {
eq() { eq() {
return true return true
} }
coordsAt(element: HTMLElement) {
return element.getBoundingClientRect()
}
} }