Sample integration of input method "agda-input" for CodeMirror

cm-candidate-selector-demo.js

import {basicSetup} from 'codemirror'
import {
  autocompletion,
  completionStatus,
  setSelectedCompletion,
  currentCompletions,
  selectedCompletionIndex,
  moveCompletionSelection,
  closeBrackets,
} from '@codemirror/autocomplete'
import {Prec, StateField} from '@codemirror/state'
import {EditorView, keymap} from '@codemirror/view'

const closebracketsInputHandler = closeBrackets()[0]

const entries = await fetch('https://raw.githubusercontent.com/agda-web/agda-input/master/out/dict.json')
  .then(r => r.json())
  .then(obj => Object.entries(obj))

const buckets = {}
for (const [seq, v] of entries) {
  const p = seq.slice(0, 1)
  buckets[p] ??= []
  buckets[p].push([seq.slice(1), v])
}

const myCloseBrackets = EditorView.inputHandler.of((view, from, to, insert) => {
  const cmplStatus = completionStatus(view.state)
  if (cmplStatus === 'active') return false
  return closebracketsInputHandler.value(view, from, to, insert)
})

let completionState
let completionConfig
{
  const ac = autocompletion()
  completionState = ac.filter(x => x instanceof StateField)[0]
  completionConfig = ac.filter(x => 'facet' in x)[0].facet
}

function myMoveCompletionSelection(forward, leftRight) {
  return view => {
    let cState = view.state.field(completionState, false)
    if (!cState || !cState.open || cState.open.disabled ||
        Date.now() - cState.open.timestamp < view.state.facet(completionConfig).interactionDelay)
      return false

    const comps = currentCompletions(view.state)
    const compidx = selectedCompletionIndex(view.state)
    const comp = comps[compidx]

    if (leftRight) {
      if (!comp.grouped) return false
      // keep the cursor within group
      let target
      if (forward && comp.groupIndex == comp.groupLen - 1) {
        target = compidx - comp.groupIndex
      } else if (!forward && comp.groupIndex == 0) {
        target = compidx + comp.groupLen - 1
      }
      if (target != null) {
        view.dispatch({
          effects: setSelectedCompletion(target),
        })
        return true
      } else {
        return moveCompletionSelection(forward)(view)
      }
    }

    // the calculation on cursor motion is horrible
    let target
    const inc = forward ? 1 : -1
    if (comp.grouped) {
      const grpmin = compidx - comp.groupIndex
      const grpmax = grpmin + comp.groupLen
      let hasNextRow = false
      for (let i = compidx + inc; i >= grpmin && i < grpmax; i += inc) {
        if (comps[i].grouped && comps[i].col == 0) {
          hasNextRow = true
        }
        if (comps[i].col == comp.col) {
          target = i
          break
        }
      }
      if (target == null) {
        if (forward) {
          // leave the group if on last row; clip otherwise
          target = hasNextRow ? grpmax - 1 : grpmax
          if (target >= comps.length) {
            target = 0
          }
        } else {
          target = grpmin - 1
        }
      }
    } else {
      for (let i = compidx + inc; i >= 0 && i < comps.length; i += inc) {
        if (!comps[i].grouped || comps[i].col == 0) {
          target = i
          break
        }
      }
      if (target == null) {
        target = forward ? 0 : comps.length - 1
        while (comps[target].grouped && comps[target].col != 0)
          target--
      }
    }
    view.dispatch({
      effects: setSelectedCompletion(target),
    })
    return true
  }
}

// cache keys that contain "\"
const entriesContainingBS = entries.filter(([k]) => k.indexOf('\\') >= 0)
console.log(entriesContainingBS)

function agdaInput(context) {
  console.log('context', context)
  // TODO: list all possible char in dict
  let match = context.matchBefore(/\\[^\\]*\\[^\\]*/)
  if (match == null || entriesContainingBS.every(([k]) => !k.startsWith(match.text.slice(1)))) {
    // fallback to find the nearest "\" and complete from there
    match = context.matchBefore(/\\[^\\]*/)
  }
  if (match == null) return null

  const before = match

  const tokenText = before.text.slice(1)

  if (tokenText.length == 0) {
    return {
      from: before ? before.from : context.pos,
      options: [{label: '\\', detail: 'Enter more...'}],
    }
  }

  const cands = buckets[tokenText[0]]  // entries.filter(([k]) => k.startsWith(tokenText))
  console.log('cands', before, cands)

  const completions = cands.map(([k, vs]) => {
    const grouped = vs.length > 1
    const label = `\\${tokenText[0]}${k}`
    const CAND_PER_ROW = 8


    return (grouped ? [{
      class: 'agda-input dummy',
      label,
      dummy: true,
      apply: vs[0],
    }] : []).concat(vs.map((v, i) => {
      const detail =
        // TODO: space char is better described by names
        v.match(/\p{Z}/u) ? `(${v})` :
        v.match(/\p{Mn}/u) ? `\u25cc${v}` : v

      return {
        grouped,
        col: i % CAND_PER_ROW,
        groupIndex: grouped ? i : -1,
        groupLen: vs.length,
        label,
        detail,
        apply: v,
        class: 'agda-input' +
          (grouped ? ' grouped' : '') +
          (i % CAND_PER_ROW == 0 ? ' leftmost' : ''),
      }
    }))
  }).flat()
  console.log('opts', completions)

  return {
    from: before ? before.from : context.pos,
    options: completions,
    validFor: /^\\[ \S]{2,}$/
  }
}

const completionTheme = EditorView.theme({
  '.cm-content': {
    fontFamily: 'JuliaMono, monospace',
  },
  '.cm-tooltip.cm-tooltip-autocomplete > ul': {
    boxSizing: 'border-box',
    display: 'grid',
    gridTemplateColumns: '.5em repeat(8, 1fr)',
  },
  '.cm-tooltip.cm-tooltip-autocomplete > ul > li': {
    gridColumn: '1 / -1',
  },
  '.agda-input': {
    width: '100%',
    display: 'flex',
    flexWrap: 'wrap',
    boxSizing: 'inherit',
  },
  ['.cm-completionListIncompleteTop::before, ' +
   '.cm-completionListIncompleteBottom::after']: {
    gridColumn: '1 / -1',
  },
  '.cm-tooltip.cm-tooltip-autocomplete > ul > li.agda-input.grouped': {
    gridColumn: 'auto',
  },
  '.agda-input .cm-completionIcon': {
    display: 'none',
  },
  '.agda-input.grouped .cm-completionLabel': {
    display: 'none',
  },
  '.agda-input .cm-completionLabel': {
    fontFamily: 'JuliaMono, monospace',
    fontSize: '14px',
  },
  '.agda-input .cm-completionDetail': {
    fontStyle: 'normal',
    fontFamily: 'JuliaMono, monospace',
    order: '-1',
    display: 'inline-block',
    textAlign: 'center',
    minWidth: '20px',
    marginRight: '.5em',
    backgroundColor: 'rgba(0, 0, 0, .05)',
  },
  '.agda-input.grouped .cm-completionDetail': {
    marginLeft: '.125em',
    marginRight: '.125em',
  },
  '.cm-tooltip.cm-tooltip-autocomplete > ul > li.agda-input.grouped.leftmost': {
    gridColumnStart: '2',
  },
  '.agda-input.dummy': {
    color: '#666',
    background: 'rgba(0, 0, 0, .1)',
  },
})

let view = new EditorView({
  doc: "type '\\'...\n",
  extensions: [
    Prec.highest(keymap.of([
      {key: 'ArrowDown',  run: myMoveCompletionSelection(true)},
      {key: 'ArrowUp',    run: myMoveCompletionSelection(false)},
      {key: 'ArrowRight', run: myMoveCompletionSelection(true, true)},
      {key: 'ArrowLeft',  run: myMoveCompletionSelection(false, true)},
    ])),
    basicSetup.map(exts => {
      if (Array.isArray(exts) && exts[0] === closebracketsInputHandler) {
        return exts.slice(1)
      }
      return exts
    }),
    myCloseBrackets,
    completionTheme,
    autocompletion({
      override: [agdaInput],
      closeOnBlur: false,
      optionClass: c => c.class ?? '',
      // FIXME: grouped does not show well when truncated
      maxRenderedOptions: 1e9,
    }),
  ],
  parent: document.body
})