temp. add entire vscode-lean4 extension

client/src/monaco-lean4/abbreviation/AbbreviationHoverProvider.ts

@@ -0,0 +1,48 @@
+import { Hover, HoverProvider, Position, Range, TextDocument } from 'vscode'
+import { AbbreviationProvider } from './AbbreviationProvider'
+import { AbbreviationConfig } from './config'
+
+/**
+ * Adds hover behaviour for getting translations of unicode characters.
+ * Eg: "Type ⊓ using \glb or \sqcap"
+ */
+export class AbbreviationHoverProvider implements HoverProvider {
+    constructor(
+        private readonly config: AbbreviationConfig,
+        private readonly abbreviations: AbbreviationProvider,
+    ) {}
+
+    provideHover(document: TextDocument, pos: Position): Hover | undefined {
+        const context = document.lineAt(pos.line).text.substr(pos.character)
+        const symbolsAtCursor = this.abbreviations.findSymbolsIn(context)
+        const allAbbrevs = symbolsAtCursor.map(symbol => ({
+            symbol,
+            abbrevs: this.abbreviations.getAllAbbreviations(symbol),
+        }))
+
+        if (allAbbrevs.length === 0 || allAbbrevs.every(a => a.abbrevs.length === 0)) {
+            return undefined
+        }
+
+        const leader = this.config.abbreviationCharacter.get()
+
+        const hoverMarkdown = allAbbrevs
+            .map(({ symbol, abbrevs }) => {
+                const abbrevInfo = `Type ${symbol} using ${abbrevs.map(a => '`' + leader + a + '`').join(' or ')}`
+                const autoClosingAbbrevs = this.abbreviations.findAutoClosingAbbreviations(symbol)
+                const autoClosingInfo =
+                    autoClosingAbbrevs.length === 0
+                        ? ''
+                        : `. ${symbol} can be auto-closed with ${autoClosingAbbrevs
+                              .map(([a, closingSym]) => `${closingSym} using \`${leader}${a}\``)
+                              .join(' or ')}.`
+                return abbrevInfo + autoClosingInfo
+            })
+            .join('\n\n')
+
+        const maxSymbolLength = Math.max(...allAbbrevs.map(a => a.symbol.length))
+        const hoverRange = new Range(pos, pos.translate(0, maxSymbolLength))
+
+        return new Hover(hoverMarkdown, hoverRange)
+    }
+}

client/src/monaco-lean4/abbreviation/AbbreviationProvider.ts

@@ -0,0 +1,118 @@
+import { computed } from 'mobx'
+import { Disposable, EventEmitter, TextEditor } from 'vscode'
+import { autorunDisposable } from '../utils/autorunDisposable'
+import * as abbreviations from './abbreviations.json'
+import { AbbreviationConfig, SymbolsByAbbreviation } from './config'
+
+/**
+ * Answers queries to a database of abbreviations.
+ */
+export class AbbreviationProvider implements Disposable {
+    private readonly disposables = new Array<Disposable>()
+    private cache: Record<string, string | undefined> = {}
+
+    private abbreviationCompletedEmitter = new EventEmitter<TextEditor>()
+    abbreviationCompleted = this.abbreviationCompletedEmitter.event
+
+    constructor(private readonly config: AbbreviationConfig) {
+        this.disposables.push(
+            autorunDisposable(() => {
+                // For the livetime of this component, cache the computed's
+                const _ = this.symbolsByAbbreviation
+                // clear cache on change
+                this.cache = {}
+            }),
+        )
+    }
+
+    onAbbreviationsCompleted(editor: TextEditor): void {
+        this.abbreviationCompletedEmitter.fire(editor)
+    }
+
+    @computed
+    get symbolsByAbbreviation(): SymbolsByAbbreviation {
+        // There are only like 1000 symbols. Building an index is not required yet.
+        return {
+            ...abbreviations,
+            ...this.config.inputModeCustomTranslations.get(),
+        }
+    }
+
+    getAllAbbreviations(symbol: string): string[] {
+        return Object.entries(this.symbolsByAbbreviation)
+            .filter(([abbr, sym]) => sym === symbol)
+            .map(([abbr]) => abbr)
+    }
+
+    findAutoClosingAbbreviations(openingSymbol: string): [string, string][] {
+        return Object.entries(this.symbolsByAbbreviation)
+            .filter(([_, sym]) => sym.startsWith(`${openingSymbol}$CURSOR`))
+            .map(([abbr, sym]) => [abbr, sym.replace(`${openingSymbol}$CURSOR`, '')])
+    }
+
+    findSymbolsIn(symbolPlusUnknown: string): string[] {
+        const result = new Set<string>()
+        for (const [abbr, sym] of Object.entries(this.symbolsByAbbreviation)) {
+            if (symbolPlusUnknown.startsWith(sym)) {
+                result.add(sym)
+            }
+        }
+        return [...result.values()]
+    }
+
+    /**
+     * Computes the replacement text for a typed abbreviation (excl. leader).
+     * This converts the longest non-empty prefix with the best-matching abbreviation.
+     *
+     * For example:
+     *   getReplacementText("alp") returns "α"
+     *   getReplacementText("alp7") returns "α7"
+     *   getReplacementText("") returns undefined
+     */
+    getReplacementText(abbrev: string): string | undefined {
+        if (abbrev in this.cache) {
+            return this.cache[abbrev]
+        }
+        const result = this._getReplacementText(abbrev)
+        this.cache[abbrev] = result
+        return result
+    }
+
+    private _getReplacementText(abbrev: string): string | undefined {
+        if (abbrev.length === 0) {
+            return undefined
+        }
+
+        const matchingSymbol = this.findSymbolsByAbbreviationPrefix(abbrev)[0]
+        if (matchingSymbol) {
+            return matchingSymbol
+        }
+
+        // Convert the `alp` in `\alp7`
+        const prefixReplacement = this.getReplacementText(abbrev.slice(0, abbrev.length - 1))
+        if (prefixReplacement) {
+            return prefixReplacement + abbrev.slice(abbrev.length - 1)
+        }
+
+        return undefined
+    }
+
+    getSymbolForAbbreviation(abbrev: string): string | undefined {
+        return this.symbolsByAbbreviation[abbrev]
+    }
+
+    findSymbolsByAbbreviationPrefix(abbrevPrefix: string): string[] {
+        const matchingAbbreviations = Object.keys(this.symbolsByAbbreviation).filter(abbrev =>
+            abbrev.startsWith(abbrevPrefix),
+        )
+
+        matchingAbbreviations.sort((a, b) => a.length - b.length)
+        return matchingAbbreviations.map(abbr => this.symbolsByAbbreviation[abbr])
+    }
+
+    dispose(): void {
+        for (const d of this.disposables) {
+            d.dispose()
+        }
+    }
+}

client/src/monaco-lean4/abbreviation/README.md

@@ -0,0 +1,38 @@
+# Abbreviation Feature
+
+Edit [abbreviations.json](./abbreviations.json) to add common abbreviations.
+Use `$CURSOR` to set the new location of the cursor after replacement.
+
+## Caveat
+
+If VS Code adds certain characters automatically (like `]` after typing `[`),
+ensure that each such subword is a strict prefix of another abbreviation.
+
+## Manual replacements
+
+When manually replacing an abbreviation early (using `Tab` by default), the abbreviation feature will pick the shortest abbreviation with a matching prefix. 
+If there are multiple shortest abbreviations with the same length, it picks the one that was declared first in [abbreviations.json](./abbreviations.json).
+
+### Example
+
+Assume that there are the abbreviations `[] -> A` and `[[]] -> B` and that the user wants to get the symbol `B`, so they type
+
+-   `\`, full text: `\`
+-   `[`, full text: `\[]` - this is a longest abbreviation! It gets replaced with `A`.
+-   `[`, full text: `A[]` - this is not what the user wanted.
+
+Instead, also add the abbreviation `[]_ -> A`:
+
+-   `\`, full text: `\`
+-   `[`, full text: `\[]` - this could be either `\[]` or `\[]_`.
+-   `[`, full text: `\[[]]` - this matches the longest abbreviation `[[]]`, so it gets replaced with `B`.
+
+# Demos
+
+## Eager Replacing
+
+![Eager Replacing Demo](../../media/abbreviation-eager-replacing.gif)
+
+## Multiple Cursors
+
+![Multi Cursor Demo](../../media/abbreviation-multi-cursor.gif)