[visual] Add decorations for theorem environments (#13708)

GitOrigin-RevId: ba78be534fd7efba7d8722a214d69b21b0e3917c
2026-06-11 07:00:47 +02:00 · 2023-07-18 11:16:30 +01:00
parent 176264144f
commit 7d3409cb75
10 changed files with 388 additions and 61 deletions
@@ -50,6 +50,8 @@ import { CloseBrace, OpenBrace } from '../../lezer-latex/latex.terms.mjs'
 import { FootnoteWidget } from './visual-widgets/footnote'
 import { getListItems } from '../toolbar/lists'
 import { TildeWidget } from './visual-widgets/tilde'
+import { BeginTheoremWidget } from './visual-widgets/begin-theorem'
+import { parseTheoremArguments } from '../../utils/tree-operations/theorems'

 type Options = {
  fileTreeManager: {
@@ -136,6 +138,13 @@ export const atomicDecorations = (options: Options) => {

    let listDepth = 0

+    const theoremEnvironments = new Map<string, string>([
+      ['theorem', 'Theorem'],
+      ['corollary', 'Corollary'],
+      ['lemma', 'lemma'],
+      ['proof', 'Proof'],
+    ])
+
    const preamble: {
      from: number
      to: number
@@ -322,7 +331,7 @@ export const atomicDecorations = (options: Options) => {
          }
        } else if (nodeRef.type.is('BeginEnv')) {
          // the beginning of an environment, with an environment name argument
-          const envName = getEnvironmentName(nodeRef.node, state)
+          const envName = getUnstarredEnvironmentName(nodeRef.node, state)

          if (envName) {
            switch (envName) {
@@ -398,7 +407,28 @@ export const atomicDecorations = (options: Options) => {
                }
                break
              default:
-                // do nothing
+                {
+                  const theoremName = theoremEnvironments.get(envName)
+
+                  if (theoremName && shouldDecorate(state, nodeRef)) {
+                    const argumentNode = nodeRef.node
+                      .getChild('OptionalArgument')
+                      ?.getChild('ShortOptionalArg')
+
+                    decorations.push(
+                      Decoration.replace({
+                        widget: new BeginTheoremWidget(
+                          envName,
+                          theoremName,
+                          argumentNode
+                        ),
+                        block: true,
+                      }).range(nodeRef.from, nodeRef.to)
+                    )
+                  }
+
+                  // do nothing
+                }
                break
            }
          }
@@ -447,6 +477,16 @@ export const atomicDecorations = (options: Options) => {
                }
                break
              default:
+                if (theoremEnvironments.has(envName)) {
+                  if (shouldDecorate(state, nodeRef)) {
+                    decorations.push(
+                      Decoration.replace({
+                        widget: new EndWidget(),
+                        block: true,
+                      }).range(nodeRef.from, nodeRef.to)
+                    )
+                  }
+                }
                // do nothing
                break
            }
@@ -818,6 +858,12 @@ export const atomicDecorations = (options: Options) => {
            )
            return false
          }
+        } else if (nodeRef.type.is('NewTheoremCommand')) {
+          const result = parseTheoremArguments(state, nodeRef.node)
+          if (result) {
+            const { name, label } = result
+            theoremEnvironments.set(name, label)
+          }
        } else if (nodeRef.type.is('UnknownCommand')) {
          // a command that's not defined separately by the grammar
          const commandNode = nodeRef.node
@@ -8,6 +8,7 @@ import { EditorState, Range } from '@codemirror/state'
 import { syntaxTree } from '@codemirror/language'
 import { getUnstarredEnvironmentName } from '../../utils/tree-operations/environments'
 import { centeringNodeForEnvironment } from '../../utils/tree-operations/figure'
+import { parseTheoremStyles } from '../../utils/tree-operations/theorems'
 import { Tree } from '@lezer/common'

 /**
@@ -22,6 +23,8 @@ export const markDecorations = ViewPlugin.define(
    ): DecorationSet => {
      const decorations: Range<Decoration>[] = []

+      const theoremStyles = parseTheoremStyles(state, tree)
+
      for (const { from, to } of view.visibleRanges) {
        tree?.iterate({
          from,
@@ -108,46 +111,96 @@ export const markDecorations = ViewPlugin.define(
                state
              )

-              switch (environmentName) {
-                case 'abstract':
-                case 'figure':
-                case 'table':
-                case 'verbatim':
-                case 'lstlisting':
-                  {
-                    const centered = Boolean(
-                      centeringNodeForEnvironment(nodeRef)
-                    )
+              if (environmentName) {
+                switch (environmentName) {
+                  case 'abstract':
+                  case 'figure':
+                  case 'table':
+                  case 'verbatim':
+                  case 'lstlisting':
+                    {
+                      const centered = Boolean(
+                        centeringNodeForEnvironment(nodeRef)
+                      )

-                    const lines = {
-                      start: state.doc.lineAt(nodeRef.from),
-                      end: state.doc.lineAt(nodeRef.to),
-                    }
-
-                    for (
-                      let lineNumber = lines.start.number;
-                      lineNumber <= lines.end.number;
-                      lineNumber++
-                    ) {
-                      const line = state.doc.line(lineNumber)
-
-                      const classNames = [
-                        `ol-cm-environment-${environmentName}`,
-                        'ol-cm-environment-line',
-                      ]
-
-                      if (centered) {
-                        classNames.push('ol-cm-environment-centered')
+                      const lines = {
+                        start: state.doc.lineAt(nodeRef.from),
+                        end: state.doc.lineAt(nodeRef.to),
                      }

-                      decorations.push(
-                        Decoration.line({
-                          class: classNames.join(' '),
-                        }).range(line.from)
-                      )
+                      for (
+                        let lineNumber = lines.start.number;
+                        lineNumber <= lines.end.number;
+                        lineNumber++
+                      ) {
+                        const line = state.doc.line(lineNumber)
+
+                        const classNames = [
+                          `ol-cm-environment-${environmentName}`,
+                          'ol-cm-environment-line',
+                        ]
+
+                        if (centered) {
+                          classNames.push('ol-cm-environment-centered')
+                        }
+
+                        decorations.push(
+                          Decoration.line({
+                            class: classNames.join(' '),
+                          }).range(line.from)
+                        )
+                      }
                    }
-                  }
-                  break
+                    break
+
+                  default:
+                    if (theoremStyles.has(environmentName)) {
+                      const theoremStyle = theoremStyles.get(environmentName)
+
+                      if (theoremStyle) {
+                        const lines = {
+                          start: state.doc.lineAt(nodeRef.from),
+                          end: state.doc.lineAt(nodeRef.to),
+                        }
+
+                        decorations.push(
+                          Decoration.line({
+                            class: [
+                              `ol-cm-environment-theorem-${theoremStyle}`,
+                              'ol-cm-environment-first-line',
+                            ].join(' '),
+                          }).range(lines.start.from)
+                        )
+
+                        for (
+                          let lineNumber = lines.start.number + 1;
+                          lineNumber <= lines.end.number - 1;
+                          lineNumber++
+                        ) {
+                          const line = state.doc.line(lineNumber)
+
+                          decorations.push(
+                            Decoration.line({
+                              class: [
+                                `ol-cm-environment-theorem-${theoremStyle}`,
+                                'ol-cm-environment-line',
+                              ].join(' '),
+                            }).range(line.from)
+                          )
+                        }
+
+                        decorations.push(
+                          Decoration.line({
+                            class: [
+                              `ol-cm-environment-theorem-${theoremStyle}`,
+                              'ol-cm-environment-last-line',
+                            ].join(' '),
+                          }).range(lines.start.from)
+                        )
+                      }
+                    }
+                    break
+                }
              }
            }
          },
@@ -113,7 +113,7 @@ export const visualTheme = EditorView.theme({
  },
  '.ol-cm-end': {
    fontFamily: 'var(--source-font-family)',
-    padding: '0.5em 0 1.5em',
+    paddingBottom: '1.5em',
    minHeight: '1em',
    textAlign: 'center',
    justifyContent: 'center',
@@ -144,6 +144,12 @@ export const visualTheme = EditorView.theme({
    {
      boxShadow: '0 2px 5px -3px rgb(125, 125, 125, 0.5)',
    },
+  '.ol-cm-environment-theorem-plain': {
+    fontStyle: 'italic',
+  },
+  '.ol-cm-begin-proof > .ol-cm-environment-name': {
+    fontStyle: 'italic',
+  },
  '.ol-cm-environment-padding': {
    flex: 1,
    height: '1px',
@@ -152,13 +158,20 @@ export const visualTheme = EditorView.theme({
  '.ol-cm-environment-name': {
    padding: '0 1em',
  },
-  '.ol-cm-environment-name-abstract': {
+  '.ol-cm-begin-abstract > .ol-cm-environment-name': {
    fontFamily: 'var(--visual-font-family)',
    fontSize: '1.2em',
    fontWeight: 550,
+    textTransform: 'capitalize',
  },
-  '.ol-cm-environment-name-abstract:first-letter': {
-    textTransform: 'uppercase',
+  '.ol-cm-begin-theorem > .ol-cm-environment-name': {
+    fontFamily: 'var(--visual-font-family)',
+    fontWeight: 550,
+    padding: '0 6px',
+    textTransform: 'capitalize',
+  },
+  '.ol-cm-begin-theorem > .ol-cm-environment-padding:first-of-type': {
+    flex: 0,
  },
  '.ol-cm-item': {
    paddingInlineStart: 'calc(var(--list-depth) * 2ch)',
@@ -0,0 +1,55 @@
+import { BeginWidget } from './begin'
+import { EditorView } from '@codemirror/view'
+import { SyntaxNode } from '@lezer/common'
+import { typesetNodeIntoElement } from '../utils/typeset-content'
+import { loadMathJax } from '../../../../mathjax/load-mathjax'
+
+export class BeginTheoremWidget extends BeginWidget {
+  constructor(
+    public environment: string,
+    public name: string,
+    public argumentNode?: SyntaxNode | null
+  ) {
+    super(environment)
+  }
+
+  toDOM(view: EditorView) {
+    const element = super.toDOM(view)
+    element.classList.add('ol-cm-begin-theorem')
+    return element
+  }
+
+  updateDOM(element: HTMLDivElement, view: EditorView) {
+    super.updateDOM(element, view)
+    element.classList.add('ol-cm-begin-theorem')
+    return true
+  }
+
+  eq(widget: BeginTheoremWidget) {
+    return (
+      super.eq(widget) &&
+      widget.name === this.name &&
+      widget.argumentNode === this.argumentNode
+    )
+  }
+
+  buildName(nameElement: HTMLSpanElement, view: EditorView) {
+    nameElement.textContent = this.name
+    if (this.argumentNode) {
+      const suffixElement = document.createElement('span')
+      typesetNodeIntoElement(this.argumentNode, suffixElement, view.state)
+      nameElement.append(' (', suffixElement, ')')
+
+      loadMathJax()
+        .then(async MathJax => {
+          if (!this.destroyed) {
+            await MathJax.typesetPromise([nameElement])
+            view.requestMeasure()
+          }
+        })
+        .catch(() => {
+          nameElement.classList.add('ol-cm-error')
+        })
+    }
+  }
+}
@@ -2,28 +2,16 @@ import { EditorView, WidgetType } from '@codemirror/view'
 import { placeSelectionInsideBlock } from '../selection'

 export class BeginWidget extends WidgetType {
+  destroyed = false
+
  constructor(public environment: string) {
    super()
  }

  toDOM(view: EditorView) {
+    this.destroyed = false
    const element = document.createElement('div')
-    element.classList.add('ol-cm-begin')
-    element.classList.add(`ol-cm-begin-${this.environment}`)
-
-    const leftPadding = document.createElement('span')
-    leftPadding.classList.add('ol-cm-environment-padding')
-    element.appendChild(leftPadding)
-
-    const name = document.createElement('span')
-    name.textContent = this.environment
-    name.classList.add('ol-cm-environment-name')
-    name.classList.add(`ol-cm-environment-name-${this.environment}`)
-    element.appendChild(name)
-
-    const rightPadding = document.createElement('span')
-    rightPadding.classList.add('ol-cm-environment-padding')
-    element.appendChild(rightPadding)
+    this.buildElement(element, view)

    element.addEventListener('mouseup', event => {
      event.preventDefault()
@@ -37,13 +25,46 @@ export class BeginWidget extends WidgetType {
    return widget.environment === this.environment
  }

-  updateDOM(element: HTMLDivElement) {
-    element.querySelector('.ol-cm-environment-name')!.textContent =
-      this.environment
+  updateDOM(element: HTMLDivElement, view: EditorView) {
+    this.destroyed = false
+    element.textContent = ''
+    element.className = ''
+    this.buildElement(element, view)
    return true
  }

+  destroy() {
+    this.destroyed = true
+  }
+
  ignoreEvent(event: Event): boolean {
    return event.type !== 'mouseup'
  }
+
+  buildName(name: HTMLSpanElement, view: EditorView) {
+    name.textContent = this.environment
+  }
+
+  buildElement(element: HTMLDivElement, view: EditorView) {
+    element.classList.add('ol-cm-begin', `ol-cm-begin-${this.environment}`)
+
+    const startPadding = document.createElement('span')
+    startPadding.classList.add(
+      'ol-cm-environment-padding',
+      'ol-cm-environment-start-padding'
+    )
+    element.appendChild(startPadding)
+
+    const name = document.createElement('span')
+    name.classList.add('ol-cm-environment-name')
+    this.buildName(name, view)
+    element.appendChild(name)
+
+    const endPadding = document.createElement('span')
+    endPadding.classList.add(
+      'ol-cm-environment-padding',
+      'ol-cm-environment-end-padding'
+    )
+    element.appendChild(endPadding)
+  }
 }
@@ -81,6 +81,8 @@
    InputCtrlSeq,
    IncludeCtrlSeq,
    ItemCtrlSeq,
+    NewTheoremCtrlSeq,
+    TheoremStyleCtrlSeq,
    CenteringCtrlSeq,
    BibliographyCtrlSeq,
    BibliographyStyleCtrlSeq,
@@ -240,6 +242,12 @@ KnownCommand {
    HrefCommand {
        HrefCtrlSeq optionalWhitespace? UrlArgument ShortTextArgument
    } |
+    NewTheoremCommand {
+        NewTheoremCtrlSeq "*"? optionalWhitespace? ShortTextArgument ((OptionalArgument? TextArgument) | (TextArgument OptionalArgument))
+    } |
+    TheoremStyleCommand {
+        TheoremStyleCtrlSeq optionalWhitespace? ShortTextArgument
+    } |
    VerbCommand {
        VerbCtrlSeq VerbContent
    } |
@@ -61,6 +61,8 @@ import {
  InputCtrlSeq,
  IncludeCtrlSeq,
  ItemCtrlSeq,
+  NewTheoremCtrlSeq,
+  TheoremStyleCtrlSeq,
  BibliographyCtrlSeq,
  BibliographyStyleCtrlSeq,
  CenteringCtrlSeq,
@@ -632,6 +634,8 @@ const otherKnowncommands = {
  '\\include': IncludeCtrlSeq,
  '\\item': ItemCtrlSeq,
  '\\centering': CenteringCtrlSeq,
+  '\\newtheorem': NewTheoremCtrlSeq,
+  '\\theoremstyle': TheoremStyleCtrlSeq,
  '\\bibliography': BibliographyCtrlSeq,
  '\\bibliographystyle': BibliographyStyleCtrlSeq,
  '\\maketitle': MaketitleCtrlSeq,
@@ -357,3 +357,11 @@ export function parseFigureData(
    graphicsCommandArguments,
  })
 }
+
+export const getBeginEnvSuffix = (state: EditorState, node: SyntaxNode) => {
+  const argumentNode = node
+    .getChild('OptionalArgument')
+    ?.getChild('ShortOptionalArg')
+
+  return argumentNode && state.sliceDoc(argumentNode.from, argumentNode.to)
+}
@@ -0,0 +1,71 @@
+import { EditorState } from '@codemirror/state'
+import { SyntaxNode, Tree } from '@lezer/common'
+import {
+  LongArg,
+  ShortArg,
+  ShortTextArgument,
+  TextArgument,
+} from '../../lezer-latex/latex.terms.mjs'
+
+export const parseTheoremArguments = (
+  state: EditorState,
+  node: SyntaxNode
+): { name: string; label: string } | undefined => {
+  const nameArgumentNode = node.getChild(ShortTextArgument)?.getChild(ShortArg)
+  const labelArgumentNode = node.getChild(TextArgument)?.getChild(LongArg)
+
+  if (nameArgumentNode && labelArgumentNode) {
+    const name = state
+      .sliceDoc(nameArgumentNode.from, nameArgumentNode.to)
+      .trim()
+
+    const label = state
+      .sliceDoc(labelArgumentNode.from, labelArgumentNode.to)
+      .trim()
+
+    if (name && label) {
+      return { name, label }
+    }
+  }
+}
+
+export const parseTheoremStyles = (state: EditorState, tree: Tree) => {
+  // TODO: only scan for styles if amsthm is present?
+  let currentTheoremStyle = 'plain'
+  const theoremStyles = new Map<string, string>()
+  const topNode = tree.topNode
+  if (topNode && topNode.name === 'LaTeX') {
+    const textNode = topNode.getChild('Text')
+    const topLevelCommands = textNode
+      ? textNode.getChildren('Command')
+      : topNode.getChildren('Command')
+    for (const command of topLevelCommands) {
+      const node = command.getChild('KnownCommand')?.getChild('$Command')
+      if (node) {
+        if (node.type.is('TheoremStyleCommand')) {
+          const theoremStyle = argumentNodeContent(state, node)
+          if (theoremStyle) {
+            currentTheoremStyle = theoremStyle
+          }
+        } else if (node.type.is('NewTheoremCommand')) {
+          const theoremEnvironmentName = argumentNodeContent(state, node)
+          if (theoremEnvironmentName) {
+            theoremStyles.set(theoremEnvironmentName, currentTheoremStyle)
+          }
+        }
+      }
+    }
+  }
+  return theoremStyles
+}
+
+const argumentNodeContent = (
+  state: EditorState,
+  node: SyntaxNode
+): string | null => {
+  const argumentNode = node.getChild(ShortTextArgument)?.getChild(ShortArg)
+
+  return argumentNode
+    ? state.sliceDoc(argumentNode.from, argumentNode.to)
+    : null
+}
@@ -540,6 +540,54 @@ describe('<CodeMirrorEditor/> in Visual mode', function () {
    })
  })

+  describe('decorates theorems', function () {
+    it('decorates a proof environment', function () {
+      cy.get('@first-line').type(
+        ['\\begin{{}proof}{Enter}', 'foo{Enter}', '\\end{{}proof}{Enter}'].join(
+          ''
+        )
+      )
+      cy.get('.cm-content').should('have.text', 'Prooffoo')
+    })
+
+    it('decorates a theorem environment', function () {
+      cy.get('@first-line').type(
+        [
+          '\\begin{{}theorem}{Enter}',
+          'foo{Enter}',
+          '\\end{{}theorem}{Enter}',
+        ].join('')
+      )
+      cy.get('.cm-content').should('have.text', 'Theoremfoo')
+    })
+
+    it('decorates a theorem environment with a label', function () {
+      cy.get('@first-line').type(
+        [
+          '\\begin{{}theorem}[Bar]{Enter}',
+          'foo{Enter}',
+          '\\end{{}theorem}{Enter}',
+        ].join('')
+      )
+      cy.get('.cm-content').should('have.text', 'Theorem (Bar)foo')
+    })
+
+    it('decorates a custom theorem environment with a label', function () {
+      cy.get('@first-line').type(
+        [
+          '\\newtheorem{{}thm}{{}Foo}{Enter}',
+          '\\begin{{}thm}[Bar]{Enter}',
+          'foo{Enter}',
+          '\\end{{}thm}{Enter}',
+        ].join('')
+      )
+      cy.get('.cm-content').should(
+        'have.text',
+        ['\\newtheorem{thm}{Foo}', 'Foo (Bar)foo'].join('')
+      )
+    })
+  })
+
  // TODO: \input
  // TODO: Math
  // TODO: Abstract