From 3cc8a85d28bf42ca3254f1458b725f77251d33d0 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 2 May 2024 17:18:45 +0200 Subject: [PATCH] temp. add entire vscode-lean4 extension --- .../abbreviation/AbbreviationHoverProvider.ts | 48 + .../abbreviation/AbbreviationProvider.ts | 118 ++ .../src/monaco-lean4/abbreviation/README.md | 38 + .../abbreviation/abbreviations.json | 1835 +++++++++++++++++ .../src/monaco-lean4/abbreviation/config.ts | 30 + client/src/monaco-lean4/abbreviation/index.ts | 34 + .../rewriter/AbbreviationRewriter.ts | 329 +++ .../rewriter/AbbreviationRewriterFeature.ts | 54 + .../abbreviation/rewriter/Range.ts | 95 + .../rewriter/TrackedAbbreviation.ts | 90 + client/src/monaco-lean4/config.ts | 294 +++ client/src/monaco-lean4/docview.ts | 428 ++++ client/src/monaco-lean4/exports.ts | 17 + client/src/monaco-lean4/extension.ts | 259 +++ client/src/monaco-lean4/infoview.ts | 895 ++++++++ client/src/monaco-lean4/leanclient.ts | 723 +++++++ client/src/monaco-lean4/projectinit.ts | 315 +++ client/src/monaco-lean4/projectoperations.ts | 363 ++++ client/src/monaco-lean4/rpc.ts | 104 + client/src/monaco-lean4/taskgutter.ts | 148 ++ .../src/monaco-lean4/utils/VsCodeSetting.ts | 134 ++ client/src/monaco-lean4/utils/assert.ts | 7 + .../monaco-lean4/utils/autorunDisposable.ts | 19 + client/src/monaco-lean4/utils/batch.ts | 227 ++ .../src/monaco-lean4/utils/clientProvider.ts | 413 ++++ .../monaco-lean4/utils/configwatchservice.ts | 145 ++ client/src/monaco-lean4/utils/converters.ts | 134 ++ client/src/monaco-lean4/utils/elan.ts | 6 + client/src/monaco-lean4/utils/errors.ts | 9 + client/src/monaco-lean4/utils/exturi.ts | 149 ++ client/src/monaco-lean4/utils/fromResource.ts | 78 + client/src/monaco-lean4/utils/fsHelper.ts | 31 + client/src/monaco-lean4/utils/lake.ts | 96 + .../src/monaco-lean4/utils/leanInstaller.ts | 361 ++++ client/src/monaco-lean4/utils/logger.ts | 31 + client/src/monaco-lean4/utils/manifest.ts | 151 ++ client/src/monaco-lean4/utils/projectInfo.ts | 136 ++ .../monaco-lean4/utils/setupDiagnostics.ts | 41 + client/src/monaco-lean4/utils/tempFolder.ts | 28 + 39 files changed, 8413 insertions(+) create mode 100644 client/src/monaco-lean4/abbreviation/AbbreviationHoverProvider.ts create mode 100644 client/src/monaco-lean4/abbreviation/AbbreviationProvider.ts create mode 100644 client/src/monaco-lean4/abbreviation/README.md create mode 100644 client/src/monaco-lean4/abbreviation/abbreviations.json create mode 100644 client/src/monaco-lean4/abbreviation/config.ts create mode 100644 client/src/monaco-lean4/abbreviation/index.ts create mode 100644 client/src/monaco-lean4/abbreviation/rewriter/AbbreviationRewriter.ts create mode 100644 client/src/monaco-lean4/abbreviation/rewriter/AbbreviationRewriterFeature.ts create mode 100644 client/src/monaco-lean4/abbreviation/rewriter/Range.ts create mode 100644 client/src/monaco-lean4/abbreviation/rewriter/TrackedAbbreviation.ts create mode 100644 client/src/monaco-lean4/config.ts create mode 100644 client/src/monaco-lean4/docview.ts create mode 100644 client/src/monaco-lean4/exports.ts create mode 100644 client/src/monaco-lean4/extension.ts create mode 100644 client/src/monaco-lean4/infoview.ts create mode 100644 client/src/monaco-lean4/leanclient.ts create mode 100644 client/src/monaco-lean4/projectinit.ts create mode 100644 client/src/monaco-lean4/projectoperations.ts create mode 100644 client/src/monaco-lean4/rpc.ts create mode 100644 client/src/monaco-lean4/taskgutter.ts create mode 100644 client/src/monaco-lean4/utils/VsCodeSetting.ts create mode 100644 client/src/monaco-lean4/utils/assert.ts create mode 100644 client/src/monaco-lean4/utils/autorunDisposable.ts create mode 100644 client/src/monaco-lean4/utils/batch.ts create mode 100644 client/src/monaco-lean4/utils/clientProvider.ts create mode 100644 client/src/monaco-lean4/utils/configwatchservice.ts create mode 100644 client/src/monaco-lean4/utils/converters.ts create mode 100644 client/src/monaco-lean4/utils/elan.ts create mode 100644 client/src/monaco-lean4/utils/errors.ts create mode 100644 client/src/monaco-lean4/utils/exturi.ts create mode 100644 client/src/monaco-lean4/utils/fromResource.ts create mode 100644 client/src/monaco-lean4/utils/fsHelper.ts create mode 100644 client/src/monaco-lean4/utils/lake.ts create mode 100644 client/src/monaco-lean4/utils/leanInstaller.ts create mode 100644 client/src/monaco-lean4/utils/logger.ts create mode 100644 client/src/monaco-lean4/utils/manifest.ts create mode 100644 client/src/monaco-lean4/utils/projectInfo.ts create mode 100644 client/src/monaco-lean4/utils/setupDiagnostics.ts create mode 100644 client/src/monaco-lean4/utils/tempFolder.ts diff --git a/client/src/monaco-lean4/abbreviation/AbbreviationHoverProvider.ts b/client/src/monaco-lean4/abbreviation/AbbreviationHoverProvider.ts new file mode 100644 index 00000000..af55fdba --- /dev/null +++ b/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) + } +} diff --git a/client/src/monaco-lean4/abbreviation/AbbreviationProvider.ts b/client/src/monaco-lean4/abbreviation/AbbreviationProvider.ts new file mode 100644 index 00000000..6c35e023 --- /dev/null +++ b/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() + private cache: Record = {} + + private abbreviationCompletedEmitter = new EventEmitter() + 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() + 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() + } + } +} diff --git a/client/src/monaco-lean4/abbreviation/README.md b/client/src/monaco-lean4/abbreviation/README.md new file mode 100644 index 00000000..51148989 --- /dev/null +++ b/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) diff --git a/client/src/monaco-lean4/abbreviation/abbreviations.json b/client/src/monaco-lean4/abbreviation/abbreviations.json new file mode 100644 index 00000000..3b9a5dc1 --- /dev/null +++ b/client/src/monaco-lean4/abbreviation/abbreviations.json @@ -0,0 +1,1835 @@ +{ + "{}": "{$CURSOR}", + "{}_": "{$CURSOR}_", + "{{}}": "⦃$CURSOR⦄", + "[]": "[$CURSOR]", + "[]_": "[$CURSOR]_", + "[[]]": "⟦$CURSOR⟧", + "<>": "⟨$CURSOR⟩", + "()": "($CURSOR)", + "()_": "($CURSOR)_", + "([])'": "⟮$CURSOR⟯", + "f<>": "‹$CURSOR›", + "f<<>>": "«$CURSOR»", + "[--]": "⁅$CURSOR⁆", + "nnnorm": "‖$CURSOR‖₊", + "norm": "‖$CURSOR‖", + "floor": "⌊$CURSOR⌋", + "ceil": "⌈$CURSOR⌉", + "nfloor": "⌊$CURSOR⌋₊", + "nceil": "⌈$CURSOR⌉₊", + "\\": "\\", + "a": "α", + "b": "β", + "c": "χ", + "d": "↓", + "e": "ε", + "g": "γ", + "i": "∩", + "m": "μ", + "n": "¬", + "o": "∘", + "p": "Π", + "t": "▸", + "r": "→", + "u": "↑", + "v": "∨", + "x": "×", + "-": "⁻¹", + "~": "∼", + ".": "·", + "*": "⋆", + "?": "¿", + "1": "₁", + "2": "₂", + "3": "₃", + "4": "₄", + "5": "₅", + "6": "₆", + "7": "₇", + "8": "₈", + "9": "₉", + "0": "₀", + "l": "←", + "<": "⟨", + ">": "⟩", + "O": "Ø", + "&": "⅋", + "A": "𝔸", + "C": "ℂ", + "D": "Δ", + "F": "𝔽", + "G": "Γ", + "H": "ℍ", + "I": "⋂", + "I0": "⋂₀", + "K": "𝕂", + "L": "Λ", + "N": "ℕ", + "P": "Π", + "Q": "ℚ", + "R": "ℝ", + "S": "Σ", + "U": "⋃", + "U0": "⋃₀", + "Z": "ℤ", + "#": "♯", + ":": "∶", + "|": "∣", + "!": "¡", + "be": "β", + "ga": "γ", + "de": "δ", + "ep": "ε", + "ze": "ζ", + "et": "η", + "th": "θ", + "io": "ι", + "ka": "κ", + "la": "λ", + "mu": "μ", + "nu": "ν", + "xi": "ξ", + "pi": "π", + "rh": "ρ", + "vsi": "ς", + "si": "σ", + "ta": "τ", + "ph": "φ", + "ch": "χ", + "ps": "ψ", + "om": "ω", + "`A": "À", + "'A": "Á", + "^{A}": "Â", + "~A": "Ã", + "\"A": "Ä", + "cC": "Ç", + "`E": "È", + "'E": "É", + "^{E}": "Ê", + "\"E": "Ë", + "`I": "Ì", + "'I": "Í", + "^{I}": "Î", + "\"I": "Ï", + "~N": "Ñ", + "`O": "Ò", + "'O": "Ó", + "^{O}": "Ô", + "~O": "Õ", + "\"O": "Ö", + "/O": "Ø", + "`U": "Ù", + "'U": "Ú", + "^{U}": "Û", + "\"U": "Ü", + "'Y": "Ý", + "`a": "à", + "'a": "á", + "^{a}": "â", + "~a": "ã", + "\"a": "ä", + "cc": "ç", + "`e": "è", + "'e": "é", + "^{e}": "ê", + "\"e": "ë", + "`i": "ì", + "'i": "í", + "^{i}": "î", + "\"i": "ï", + "~{n}": "ñ", + "`o": "ò", + "'o": "ó", + "^{o}": "ô", + "~o": "õ", + "\"o": "ö", + "/o": "ø", + "`u": "ù", + "'u": "ú", + "^{u}": "û", + "\"u": "ü", + "'y": "ý", + "\"y": "ÿ", + "/L": "Ł", + "notin": "∉", + "note": "♩", + "not": "¬", + "nomisma": "𐆎", + "nin": "∉", + "nni": "∌", + "ni": "∋", + "nattrans": "⟹", + "nat_trans": "⟹", + "natural": "♮", + "nat": "ℕ", + "naira": "₦", + "nabla": "∇", + "napprox": "≉", + "numero": "№", + "nLeftarrow": "⇍", + "nLeftrightarrow": "⇎", + "nRightarrow": "⇏", + "nVDash": "⊯", + "nVdash": "⊮", + "ncong": "≇", + "nearrow": "↗", + "neg": "¬", + "nequiv": "≢", + "neq": "≠", + "nexists": "∄", + "ne": "≠", + "ngeqq": "≱", + "ngeqslant": "≱", + "ngeq": "≱", + "ngtr": "≯", + "nleftarrow": "↚", + "nleftrightarrow": "↮", + "nleqq": "≰", + "nleqslant": "≰", + "nleq": "≰", + "nless": "≮", + "nmid": "∤", + "nparallel": "∦", + "npreceq": "⋠", + "nprec": "⊀", + "nrightarrow": "↛", + "nshortmid": "∤", + "nsimeq": "≄", + "nsim": "≁", + "nsubseteqq": "⊈", + "nsubseteq": "⊈", + "nsubset": "⊄", + "nsucceq": "⋡", + "nsucc": "⊁", + "nsupseteqq": "⊉", + "nsupseteq": "⊉", + "nsupset": "⊅", + "ntrianglelefteq": "⋬", + "ntriangleleft": "⋪", + "ntrianglerighteq": "⋭", + "ntriangleright": "⋫", + "nvDash": "⊭", + "nvdash": "⊬", + "nwarrow": "↖", + "eqn": "≠", + "equiv": "≃", + "eqcirc": "≖", + "eqcolon": "≕", + "eqslantgtr": "⋝", + "eqslantless": "⋜", + "entails": "⊢", + "en": "–", + "exn": "∄", + "exists": "∃", + "ex": "∃", + "emptyset": "∅", + "empty": "∅", + "em": "—", + "epsilon": "ε", + "eps": "ε", + "euro": "€", + "eta": "η", + "ell": "ℓ", + "iso": "≅", + "in": "∈", + "inn": "∉", + "inter": "∩", + "intercal": "⊺", + "intersection": "∩", + "integral": "∫", + "integral-": "⨍", + "int": "ℤ", + "inv": "⁻¹", + "increment": "∆", + "inf": "⊓", + "infi": "⨅", + "infty": "∞", + "iff": "↔", + "imp": "→", + "imath": "ı", + "iota": "ι", + "=n": "≠", + "==n": "≢", + "===": "≣", + "==>": "⟹", + "==": "≡", + "=:": "≕", + "=o": "≗", + "=>n": "⇏", + "=>": "⇒", + "~n": "≁", + "~~n": "≉", + "~~~": "≋", + "~~-": "≊", + "~~": "≈", + "~-n": "≄", + "~-": "≃", + "~=n": "≇", + "~=": "≅", + "homotopy": "∼", + "hom": "⟶", + "hori": "ϩ", + "hookleftarrow": "↩", + "hookrightarrow": "↪", + "hryvnia": "₴", + "heta": "ͱ", + "heartsuit": "♥", + "hbar": "ℏ", + ":~": "∻", + ":=": "≔", + "::-": "∺", + "::": "∷", + "-~": "≂", + "-|": "⊣", + "-1": "⁻¹", + "^-1": "⁻¹", + "-2": "⁻²", + "-3": "⁻³", + "-:": "∹", + "->n": "↛", + "->": "→", + "-->": "⟶", + "---": "─", + "--=": "═", + "--_": "━", + "--.": "╌", + "-o": "⊸", + ".=.": "≑", + ".=": "≐", + ".+": "∔", + ".-": "∸", + "...": "⋯", + "(=": "≘", + "(b": "⟅", + "and=": "≙", + "and": "∧", + "an": "∧", + "angle": "∠", + "rightangle": "∟", + "angstrom": "Å", + "all": "∀", + "allf": "∀ᶠ", + "all^f": "∀ᶠ", + "allm": "∀ᵐ", + "all^m": "∀ᵐ", + "alpha": "α", + "aleph": "ℵ", + "aleph0": "ℵ₀", + "asterisk": "⁎", + "ast": "∗", + "asymp": "≍", + "apl": "⌶", + "approxeq": "≊", + "approx": "≈", + "aa": "å", + "ae": "æ", + "austral": "₳", + "afghani": "؋", + "amalg": "∐", + "average": "⨍", + "-int": "⨍", + "or=": "≚", + "ordfeminine": "ª", + "ordmasculine": "º", + "or": "∨", + "oplus": "⊕", + "od": "ᵒᵈ", + "orderdual": "ᵒᵈ", + "addopposite": "ᵃᵒᵖ", + "aop": "ᵃᵒᵖ", + "mulopposite": "ᵐᵒᵖ", + "mop": "ᵐᵒᵖ", + "opposite": "ᵒᵖ", + "op": "ᵒᵖ", + "o+": "⊕", + "o--": "⊖", + "o-": "⊝", + "ox": "⊗", + "o/": "⊘", + "o.": "⊙", + "oo": "⊚", + "o*": "∘*", + "o=": "⊜", + "oe": "œ", + "octagonal": "🛑", + "ohm": "Ω", + "ounce": "℥", + "omega": "ω", + "omicron": "ο", + "ominus": "⊖", + "odot": "⊙", + "oint": "∮", + "oiint": "∯", + "oslash": "⊘", + "otimes": "⊗", + "tensorproduct": "⊗", + "pitensorproduct": "⨂", + "tensorpower": "⨂", + "pd": "∂", + "*=": "≛", + "t=": "≜", + "tint": "∯", + "transport": "▹", + "trans": "▹", + "triangledown": "▿", + "trianglelefteq": "⊴", + "triangleleft": "◃", + "triangleq": "≜", + "trianglerighteq": "⊵", + "triangleright": "▹", + "triangle": "▵", + "tr": "⬝", + "tb": "◂", + "twoheadleftarrow": "↞", + "twoheadrightarrow": "↠", + "tw": "◃", + "tie": "⁀", + "times": "×", + "theta": "θ", + "therefore": "∴", + "thickapprox": "≈", + "thicksim": "∼", + "telephone": "℡", + "tenge": "₸", + "textmusicalnote": "♪", + "textmu": "µ", + "textfractionsolidus": "⁄", + "textbaht": "฿", + "textdied": "✝", + "textdiscount": "⁒", + "textcolonmonetary": "₡", + "textcircledP": "℗", + "textwon": "₩", + "textnaira": "₦", + "textnumero": "№", + "textpeso": "₱", + "textpertenthousand": "‱", + "textlira": "₤", + "textlquill": "⁅", + "textrecipe": "℞", + "textreferencemark": "※", + "textrquill": "⁆", + "textinterrobang": "‽", + "textestimated": "℮", + "textopenbullet": "◦", + "tugrik": "₮", + "tau": "τ", + "top": "⊤", + "to": "→", + + "to0": "→₀", + "r0": "→₀", + "to_0": "→₀", + "r_0": "→₀", + "finsupp": "→₀", + "to1": "→₁", + "r1": "→₁", + "to_1": "→₁", + "r_1": "→₁", + "l1": "→₁", + "to1s": "→₁ₛ", + "r1s": "→₁ₛ", + "to_1s": "→₁ₛ", + "r_1s": "→₁ₛ", + "l1simplefunc": "→₁ₛ", + "toa": "→ₐ", + "ra": "→ₐ", + "to_a": "→ₐ", + "r_a": "→ₐ", + "alghom": "→ₐ", + "tob": "→ᵇ", + "rb": "→ᵇ", + "to^b": "→ᵇ", + "r^b": "→ᵇ", + "boundedcontinuousfunction": "→ᵇ", + "tol": "→ₗ", + "rl": "→ₗ", + "to_l": "→ₗ", + "r_l": "→ₗ", + "linearmap": "→ₗ", + "tom": "→ₘ", + "rm": "→ₘ", + "to_m": "→ₘ", + "r_m": "→ₘ", + "aeeqfun": "→ₘ", + "rp": "→ₚ", + "to_p": "→ₚ", + "r_p": "→ₚ", + "dfinsupp": "→ₚ", + "tos": "→ₛ", + "rs": "→ₛ", + "to_s": "→ₛ", + "r_s": "→ₛ", + "simplefunc": "→ₛ", + "heyting": "⇨", + "himp": "⇨", + "hnot": "￢", + + "covers": "⋖", + "covby": "⋖", + "wcovby": "⩿", + "wcovers": "⩿", + "def=": "≝", + "defs": "≙", + "degree": "°", + "dei": "ϯ", + "delta": "δ", + "doteqdot": "≑", + "doteq": "≐", + "dotplus": "∔", + "dotsquare": "⊡", + "dot": "⬝", + "dong": "₫", + "downarrow": "↓", + "downdownarrows": "⇊", + "downleftharpoon": "⇃", + "downrightharpoon": "⇂", + "dr-": "↘", + "dr=": "⇘", + "drachma": "₯", + "dr": "↘", + "dl-": "↙", + "dl=": "⇙", + "dl": "↙", + "d-2": "⇊", + "d-u-": "⇵", + "d-|": "↧", + "d-": "↓", + "d==": "⟱", + "d=": "⇓", + "dd-": "↡", + "ddagger": "‡", + "ddag": "‡", + "ddots": "⋱", + "dz": "↯", + "dib": "◆", + "diw": "◇", + "di.": "◈", + "die": "⚀", + "division": "÷", + "divideontimes": "⋇", + "div": "÷", + "diameter": "⌀", + "diamondsuit": "♢", + "diamond": "⋄", + "digamma": "ϝ", + "di": "◆", + "dagger": "†", + "dag": "†", + "daleth": "ℸ", + "dashv": "⊣", + "dh": "ð", + "dvd": "∣", + "m=": "≞", + "meet": "⊓", + "member": "∈", + "mem": "∈", + "measuredangle": "∡", + "mapsto": "↦", + "male": "♂", + "maltese": "✠", + "manat": "₼", + "mathscr{I}": "ℐ", + "minus": "−", + "mill": "₥", + "micro": "µ", + "mid": "∣", + "multiplication": "×", + "multimap": "⊸", + "mho": "℧", + "models": "⊧", + "mp": "∓", + "?=": "≟", + "??": "⁇", + "?!": "‽", + "prohibited": "🛇", + "prod": "∏", + "propto": "∝", + "precapprox": "≾", + "preceq": "≼", + "precnapprox": "⋨", + "precnsim": "⋨", + "precsim": "≾", + "prec": "≺", + "preim": "⁻¹'", + "preimage": "⁻¹'", + "prime": "′", + "pr": "↣", + "powerset": "𝒫", + "pounds": "£", + "pound": "£", + "pab": "▰", + "paw": "▱", + "partnership": "㉐", + "partial": "∂", + "paragraph": "¶", + "parallel": "∥", + "pa": "▰", + "pm": "±", + "perp": "⟂", + "^perp": "ᗮ", + "permil": "‰", + "per": "⅌", + "peso": "₱", + "peseta": "₧", + "pilcrow": "¶", + "pitchfork": "⋔", + "psi": "ψ", + "phi": "φ", + "8<": "✂", + "leqn": "≰", + "leqq": "≦", + "leqslant": "≤", + "leq": "≤", + "len": "≰", + "leadsto": "↝", + "leftarrowtail": "↢", + "leftarrow": "←", + "leftharpoondown": "↽", + "leftharpoonup": "↼", + "leftleftarrows": "⇇", + "leftrightarrows": "⇆", + "leftrightarrow": "↔", + "leftrightharpoons": "⇋", + "leftrightsquigarrow": "↭", + "leftthreetimes": "⋋", + "lessapprox": "≲", + "lessdot": "⋖", + "lesseqgtr": "⋚", + "lesseqqgtr": "⋚", + "lessgtr": "≶", + "lesssim": "≲", + "le": "≤", + "lub": "⊔", + "lr--": "⟷", + "lr-n": "↮", + "lr-": "↔", + "lr=n": "⇎", + "lr=": "⇔", + "lr~": "↭", + "lrcorner": "⌟", + "lr": "↔", + "l-2": "⇇", + "l-r-": "⇆", + "l--": "⟵", + "l-n": "↚", + "l-|": "↤", + "l->": "↢", + "l-": "←", + "l==": "⇚", + "l=n": "⇍", + "l=": "⇐", + "l~": "↜", + "ll-": "↞", + "llcorner": "⌞", + "llbracket": "〚", + "ll": "≪", + "lbag": "⟅", + "lambda": "λ", + "lamda": "λ", + "lam": "λ", + "lari": "₾", + "langle": "⟨", + "lira": "₤", + "lceil": "⌈", + "ldots": "…", + "ldq": "“", + "ldata": "《", + "lfloor": "⌊", + "lf": "⧏", + "<|": "⧏", + "lhd": "◁", + "lnapprox": "⋦", + "lneqq": "≨", + "lneq": "≨", + "lnsim": "⋦", + "lnot": "¬", + "longleftarrow": "⟵", + "longleftrightarrow": "⟷", + "longrightarrow": "⟶", + "looparrowleft": "↫", + "looparrowright": "↬", + "lozenge": "✧", + "lq": "‘", + "ltimes": "⋉", + "lvertneqq": "≨", + "geqn": "≱", + "geqq": "≧", + "geqslant": "≥", + "geq": "≥", + "gen": "≱", + "gets": "←", + "ge": "≥", + "glb": "⊓", + "glqq": "„", + "glq": "‚", + "guarani": "₲", + "gangia": "ϫ", + "gamma": "γ", + "ggg": "⋙", + "gg": "≫", + "gimel": "ℷ", + "gnapprox": "⋧", + "gneqq": "≩", + "gneq": "≩", + "gnsim": "⋧", + "gtrapprox": "≳", + "gtrdot": "⋗", + "gtreqless": "⋛", + "gtreqqless": "⋛", + "gtrless": "≷", + "gtrsim": "≳", + "gvertneqq": "≩", + "grqq": "“", + "grq": "‘", + "<=n": "≰", + "<=>n": "⇎", + "<=>": "⇔", + "<=": "≤", + "": "⋗", + "<->n": "↮", + "<->": "↔", + "<-->": "⟷", + "<--": "⟵", + "<-n": "↚", + "<-": "←", + "<<": "⟪", + ">=n": "≱", + ">=": "≥", + ">n": "≯", + ">~nn": "≵", + ">~n": "⋧", + ">~": "≳", + ">>": "⟫", + "root": "√", + "ssubn": "⊄", + "ssub": "⊂", + "ssupn": "⊅", + "ssup": "⊃", + "ssqub": "⊏", + "ssqup": "⊐", + "ss": "⊆", + "subn": "⊈", + "subseteqq": "⊆", + "subseteq": "⊆", + "subsetneqq": "⊊", + "subsetneq": "⊊", + "subset": "⊆", + "ssubset": "⊂", + "sub": "⊆", + "supn": "⊉", + "supseteqq": "⊇", + "supseteq": "⊇", + "supsetneqq": "⊋", + "supsetneq": "⊋", + "supset": "⊇", + "ssupset": "⊃", + "sUnion": "⋃₀", + "sInter": "⋂₀", + "sup": "⊔", + "supr": "⨆", + "surd3": "∛", + "surd4": "∜", + "surd": "√", + "succapprox": "≿", + "succcurlyeq": "≽", + "succeq": "≽", + "succnapprox": "⋩", + "succnsim": "⋩", + "succsim": "≿", + "succ": "≻", + "sum": "∑", + "specializes": "⤳", + "~>": "⤳", + "squbn": "⋢", + "squb": "⊑", + "squpn": "⋣", + "squp": "⊒", + "square": "□", + "squigarrowright": "⇝", + "sqb": "■", + "sqw": "□", + "sq.": "▣", + "sqo": "▢", + "sqcap": "⊓", + "sqcup": "⊔", + "sqrt": "√", + "sqsubseteq": "⊑", + "sqsubset": "⊏", + "sqsupseteq": "⊒", + "sqsupset": "⊐", + "sq": "◾", + "sy": "⁻¹", + "symmdiff": "∆", + "st4": "✦", + "st6": "✶", + "st8": "✴", + "st12": "✹", + "stigma": "ϛ", + "star": "⋆", + "straightphi": "φ", + "st": "⋆", + "spesmilo": "₷", + "spadesuit": "♠", + "sphericalangle": "∢", + "section": "§", + "searrow": "↘", + "setminus": "\\", + "san": "ϻ", + "sampi": "ϡ", + "shortmid": "∣", + "sho": "ϸ", + "shima": "ϭ", + "shei": "ϣ", + "sharp": "♯", + "sigma": "σ", + "simeq": "≃", + "sim": "∼", + "sbs": "﹨", + "smallamalg": "∐", + "smallsetminus": "∖", + "smallsmile": "⌣", + "smile": "⌣", + "smul": "•", + "swarrow": "↙", + "Tr": "◀", + "Tb": "◀", + "Tw": "◁", + "Tau": "Τ", + "Theta": "Θ", + "TH": "Þ", + "union": "∪", + "undertie": "‿", + "uncertainty": "⯑", + "un": "∪", + "u+": "⊎", + "u.": "⊍", + "ud-|": "↨", + "ud-": "↕", + "ud=": "⇕", + "ud": "↕", + "ul-": "↖", + "ul=": "⇖", + "ulcorner": "⌜", + "ul": "↖", + "ur-": "↗", + "ur=": "⇗", + "urcorner": "⌝", + "ur": "↗", + "u-2": "⇈", + "u-d-": "⇅", + "u-|": "↥", + "u-": "↑", + "u==": "⟰", + "u=": "⇑", + "uu-": "↟", + "upsilon": "υ", + "uparrow": "↑", + "updownarrow": "↕", + "upleftharpoon": "↿", + "uplus": "⊎", + "uprightharpoon": "↾", + "upuparrows": "⇈", + "And": "⋀", + "AA": "Å", + "AE": "Æ", + "Alpha": "Α", + "Or": "⋁", + "O+": "⨁", + "directsum": "⨁", + "Ox": "⨂", + "O.": "⨀", + "O*": "⍟", + "OE": "Œ", + "Omega": "Ω", + "Omicron": "Ο", + "Int": "ℤ", + "Inter": "⋂", + "bInter": "⋂", + "Iota": "Ι", + "Im": "ℑ", + "Un": "⋃", + "Union": "⋃", + "bUnion": "⋃", + "U+": "⨄", + "U.": "⨃", + "Upsilon": "Υ", + "Uparrow": "⇑", + "Updownarrow": "⇕", + "Gl-": "ƛ", + "Gl": "λ", + "Gangia": "Ϫ", + "Gamma": "Γ", + "Glb": "⨅", + "Ga": "α", + "GA": "Α", + "Gb": "β", + "GB": "Β", + "Gg": "γ", + "GG": "Γ", + "Gd": "δ", + "GD": "Δ", + "Ge": "ε", + "GE": "Ε", + "Gz": "ζ", + "GZ": "Ζ", + "Gth": "θ", + "Gt": "τ", + "GTH": "Θ", + "GT": "Τ", + "Gi": "ι", + "GI": "Ι", + "Gk": "κ", + "GK": "Κ", + "GL": "Λ", + "Gm": "μ", + "GM": "Μ", + "Gn": "ν", + "GN": "Ν", + "Gx": "ξ", + "GX": "Ξ", + "Gr": "ρ", + "GR": "Ρ", + "Gs": "σ", + "GS": "Σ", + "Gu": "υ", + "GU": "Υ", + "Gf": "φ", + "GF": "Φ", + "Gc": "χ", + "GC": "Χ", + "Gp": "ψ", + "GP": "Ψ", + "Go": "ω", + "GO": "Ω", + "Inf": "⨅", + "Join": "⨆", + "Lub": "⨆", + "Lambda": "Λ", + "Lamda": "Λ", + "Leftarrow": "⇐", + "Leftrightarrow": "⇔", + "Letter": "✉", + "Lleftarrow": "⇚", + "Ll": "⋘", + "Longleftarrow": "⇐", + "Longleftrightarrow": "⇔", + "Longrightarrow": "⇒", + "Meet": "⨅", + "Sup": "⨆", + "Sqcap": "⨅", + "Sqcup": "⨆", + "Lsh": "↰", + "|-n": "⊬", + "|-": "⊢", + "|=n": "⊭", + "|=": "⊨", + "|->": "↦", + "|=>": "⇰", + "||-n": "⊮", + "||-": "⊩", + "||=n": "⊯", + "||=": "⊫", + "|||-": "⊪", + "||": "‖", + "fuzzy": "‖", + "|n": "∤", + "Com": "ℂ", + "Chi": "Χ", + "Cap": "⋒", + "Cup": "⋓", + "cul": "⌜", + "cuL": "⌈", + "currency": "¤", + "curlyeqprec": "⋞", + "curlyeqsucc": "⋟", + "curlypreceq": "≼", + "curlyvee": "⋎", + "curlywedge": "⋏", + "curvearrowleft": "↶", + "curvearrowright": "↷", + "cur": "⌝", + "cuR": "⌉", + "cup": "∪", + "cu": "⌜", + "cll": "⌞", + "clL": "⌊", + "clr": "⌟", + "clR": "⌋", + "clubsuit": "♣", + "cl": "⌞", + "construction": "🚧", + "cong": "≅", + "con": "⬝", + "compl": "ᶜ", + "complement": "ᶜ", + "complementprefix": "∁", + "Complement": "∁", + "comp": "∘", + "com": "ℂ", + "coloneq": "≔", + "colon": "₡", + "copyright": "©", + "cdots": "⋯", + "cdot": "⬝", + "cib": "●", + "ciw": "○", + "ci..": "◌", + "ci.": "◎", + "ciO": "◯", + "circeq": "≗", + "circlearrowleft": "↺", + "circlearrowright": "↻", + "circledR": "®", + "circledS": "Ⓢ", + "circledast": "⊛", + "circledcirc": "⊚", + "circleddash": "⊝", + "circ": "∘", + "ci": "●", + "centerdot": "·", + "cent": "¢", + "cedi": "₵", + "celsius": "℃", + "ce": "ȩ", + "checkmark": "✓", + "chi": "χ", + "cruzeiro": "₢", + "caution": "☡", + "cap": "∩", + "qed": "∎", + "quad": " ", + "quot": "⧸", + "bigsolidus": "⧸", + "/": "⧸", + "+ ": "⊹", + "b+": "⊞", + "b-": "⊟", + "bx": "⊠", + "b.": "⊡", + "bn": "ℕ", + "bz": "ℤ", + "bq": "ℚ", + "brokenbar": "¦", + "br": "ℝ", + "bc": "ℂ", + "bp": "ℙ", + "bb": "𝔹", + "bsum": "⅀", + "b0": "𝟘", + "b1": "𝟙", + "b2": "𝟚", + "b3": "𝟛", + "b4": "𝟜", + "b5": "𝟝", + "b6": "𝟞", + "b7": "𝟟", + "b8": "𝟠", + "b9": "𝟡", + "sb0": "𝟬", + "sb1": "𝟭", + "sb2": "𝟮", + "sb3": "𝟯", + "sb4": "𝟰", + "sb5": "𝟱", + "sb6": "𝟲", + "sb7": "𝟳", + "sb8": "𝟴", + "sb9": "𝟵", + "bub": "•", + "buw": "◦", + "but": "‣", + "bumpeq": "≏", + "bu": "•", + "biohazard": "☣", + "bihimp": "⇔", + "bigcap": "⋂", + "bigcirc": "◯", + "bigcoprod": "∐", + "bigcup": "⋃", + "bigglb": "⨅", + "biginf": "⨅", + "bigjoin": "⨆", + "biglub": "⨆", + "bigmeet": "⨅", + "bigsqcap": "⨅", + "bigsqcup": "⨆", + "bigstar": "★", + "bigsup": "⨆", + "bigtriangledown": "▽", + "bigtriangleup": "△", + "bigvee": "⋁", + "bigwedge": "⋀", + "beta": "β", + "beth": "ℶ", + "between": "≬", + "because": "∵", + "backcong": "≌", + "backepsilon": "∍", + "backprime": "‵", + "backsimeq": "⋍", + "backsim": "∽", + "barwedge": "⊼", + "blacklozenge": "✦", + "blacksquare": "▪", + "blacksmiley": "☻", + "blacktriangledown": "▾", + "blacktriangleleft": "◂", + "blacktriangleright": "▸", + "blacktriangle": "▴", + "bot": "⊥", + "^bot": "ᗮ", + "bowtie": "⋈", + "boxminus": "⊟", + "boxmid": "◫", + "hcomp": "◫", + "boxplus": "⊞", + "boxtimes": "⊠", + "join": "⊔", + "r-2": "⇉", + "r-3": "⇶", + "r-l-": "⇄", + "r--": "⟶", + "r-n": "↛", + "r-|": "↦", + "r->": "↣", + "r-o": "⊸", + "r-": "→", + "r==": "⇛", + "r=n": "⇏", + "r=": "⇒", + "r~": "↝", + "rr-": "↠", + "reb": "▬", + "rew": "▭", + "real": "ℝ", + "registered": "®", + "re": "▬", + "rbag": "⟆", + "rat": "ℚ", + "radioactive": "☢", + "rrbracket": "〛", + "rangle": "⟩", + "rq": "’", + "rial": "﷼", + "rightarrowtail": "↣", + "rightarrow": "→", + "rightharpoondown": "⇁", + "rightharpoonup": "⇀", + "rightleftarrows": "⇄", + "rightleftharpoons": "⇌", + "rightrightarrows": "⇉", + "rightthreetimes": "⋌", + "risingdotseq": "≓", + "ruble": "₽", + "rupee": "₨", + "rho": "ρ", + "rhd": "▷", + "rceil": "⌉", + "rfloor": "⌋", + "rtimes": "⋊", + "rdq": "”", + "rdata": "》", + "functor": "⥤", + "fun": "λ", + "f<<": "«", + "f>>": "»", + "f<": "‹", + "f>": "›", + "finprod": "∏ᶠ", + "finsum": "∑ᶠ", + "frac12": "½", + "frac13": "⅓", + "frac14": "¼", + "frac15": "⅕", + "frac16": "⅙", + "frac18": "⅛", + "frac1": "⅟", + "frac23": "⅔", + "frac25": "⅖", + "frac34": "¾", + "frac35": "⅗", + "frac38": "⅜", + "frac45": "⅘", + "frac56": "⅚", + "frac58": "⅝", + "frac78": "⅞", + "frac": "¼", + "frown": "⌢", + "frqq": "»", + "frq": "›", + "female": "♀", + "fei": "ϥ", + "facsimile": "℻", + "fallingdotseq": "≒", + "flat": "♭", + "flqq": "«", + "flq": "‹", + "forall": "∀", + ")b": "⟆", + "[[": "⟦", + "]]": "⟧", + "{{": "⦃", + "}}": "⦄", + "([": "⟮", + "])": "⟯", + "Xi": "Ξ", + "Nat": "ℕ", + "Nu": "Ν", + "Zeta": "Ζ", + "Rat": "ℚ", + "Real": "ℝ", + "Re": "ℜ", + "Rho": "Ρ", + "Rightarrow": "⇒", + "Rrightarrow": "⇛", + "Rsh": "↱", + "Fei": "Ϥ", + "Frowny": "☹", + "Hori": "Ϩ", + "Heta": "Ͱ", + "Khei": "Ϧ", + "Koppa": "Ϟ", + "Kappa": "Κ", + "^a": "ᵃ", + "^b": "ᵇ", + "^c": "ᶜ", + "^d": "ᵈ", + "^e": "ᵉ", + "^f": "ᶠ", + "^g": "ᵍ", + "^h": "ʰ", + "^i": "ⁱ", + "^j": "ʲ", + "^k": "ᵏ", + "^l": "ˡ", + "^m": "ᵐ", + "^n": "ⁿ", + "^o": "ᵒ", + "^p": "ᵖ", + "^r": "ʳ", + "^s": "ˢ", + "^t": "ᵗ", + "^u": "ᵘ", + "^v": "ᵛ", + "^w": "ʷ", + "^x": "ˣ", + "^y": "ʸ", + "^z": "ᶻ", + "^A": "ᴬ", + "^B": "ᴮ", + "^D": "ᴰ", + "^E": "ᴱ", + "^G": "ᴳ", + "^H": "ᴴ", + "^I": "ᴵ", + "^J": "ᴶ", + "^K": "ᴷ", + "^L": "ᴸ", + "^M": "ᴹ", + "^N": "ᴺ", + "^O": "ᴼ", + "^P": "ᴾ", + "^R": "ᴿ", + "^T": "ᵀ", + "^U": "ᵁ", + "^V": "ⱽ", + "^W": "ᵂ", + "^0": "⁰", + "^1": "¹", + "^2": "²", + "^3": "³", + "^4": "⁴", + "^5": "⁵", + "^6": "⁶", + "^7": "⁷", + "^8": "⁸", + "^9": "⁹", + "^)": "⁾", + "^(": "⁽", + "^=": "⁼", + "^+": "⁺", + "^o_": "º", + "^-": "⁻", + "^a_": "ª", + "^uhook": "ꭟ", + "^ubar": "ᶶ", + "^upsilon": "ᶷ", + "^ltilde": "ꭞ", + "^ls": "ꭝ", + "^lhook": "ᶪ", + "^lretroflexhook": "ᶩ", + "^oe": "ꟹ", + "^heng": "ꭜ", + "^hhook": "ʱ", + "^hwithhook": "ʱ", + "^Hstroke": "ꟸ", + "^theta": "ᶿ", + "^turnedv": "ᶺ", + "^turnedmleg": "ᶭ", + "^turnedm": "ᵚ", + "^turnedh": "ᶣ", + "^turnedalpha": "ᶛ", + "^turnedae": "ᵆ", + "^turneda": "ᵄ", + "^turnedi": "ᵎ", + "^turnede": "ᵌ", + "^turnedrhook": "ʵ", + "^turnedrwithhook": "ʵ", + "^turnedr": "ʴ", + "^twithpalatalhook": "ᶵ", + "^otop": "ᵔ", + "^ezh": "ᶾ", + "^esh": "ᶴ", + "^eth": "ᶞ", + "^eng": "ᵑ", + "^zcurl": "ᶽ", + "^zretroflexhook": "ᶼ", + "^vhook": "ᶹ", + "^Ismall": "ᶦ", + "^Lsmall": "ᶫ", + "^Nsmall": "ᶰ", + "^Usmall": "ᶸ", + "^Istroke": "ᶧ", + "^Rinverted": "ʶ", + "^ccurl": "ᶝ", + "^chi": "ᵡ", + "^shook": "ᶳ", + "^gscript": "ᶢ", + "^schwa": "ᵊ", + "^usideways": "ᵙ", + "^phi": "ᶲ", + "^obarred": "ᶱ", + "^beta": "ᵝ", + "^obottom": "ᵕ", + "^nretroflexhook": "ᶯ", + "^nlefthook": "ᶮ", + "^mhook": "ᶬ", + "^jtail": "ᶨ", + "^iota": "ᶥ", + "^istroke": "ᶤ", + "^ereversedopen": "ᶟ", + "^stop": "ˤ", + "^varphi": "ᵠ", + "^vargamma": "ᵞ", + "^gamma": "ˠ", + "^ain": "ᵜ", + "^alpha": "ᵅ", + "^oopen": "ᵓ", + "^eopen": "ᵋ", + "^Ou": "ᴽ", + "^Nreversed": "ᴻ", + "^Ereversed": "ᴲ", + "^Bbarred": "ᴯ", + "^Ae": "ᴭ", + "^SM": "℠", + "^TEL": "℡", + "^TM": "™", + "_a": "ₐ", + "_e": "ₑ", + "_h": "ₕ", + "_i": "ᵢ", + "_j": "ⱼ", + "_k": "ₖ", + "_l": "ₗ", + "_m": "ₘ", + "_n": "ₙ", + "_o": "ₒ", + "_p": "ₚ", + "_r": "ᵣ", + "_s": "ₛ", + "_t": "ₜ", + "_u": "ᵤ", + "_v": "ᵥ", + "_x": "ₓ", + "_0": "₀", + "_1": "₁", + "_2": "₂", + "_3": "₃", + "_4": "₄", + "_5": "₅", + "_6": "₆", + "_7": "₇", + "_8": "₈", + "_9": "₉", + "_)": "₎", + "_(": "₍", + "_=": "₌", + "_+": "₊", + "_--": "̲", + "_-": "₋", + "!!": "‼", + "!?": "⁉", + "San": "Ϻ", + "Sampi": "Ϡ", + "Sho": "Ϸ", + "Shima": "Ϭ", + "Shei": "Ϣ", + "Stigma": "Ϛ", + "Sigma": "Σ", + "Subset": "⋐", + "Supset": "⋑", + "Smiley": "☺", + "Psi": "Ψ", + "Phi": "Φ", + "Pi": "Π", + + "Pi0": "Π₀", + "P0": "Π₀", + "Pi_0": "Π₀", + "P_0": "Π₀", + + "bfA": "𝐀", + "bfB": "𝐁", + "bfC": "𝐂", + "bfD": "𝐃", + "bfE": "𝐄", + "bfF": "𝐅", + "bfG": "𝐆", + "bfH": "𝐇", + "bfI": "𝐈", + "bfJ": "𝐉", + "bfK": "𝐊", + "bfL": "𝐋", + "bfM": "𝐌", + "bfN": "𝐍", + "bfO": "𝐎", + "bfP": "𝐏", + "bfQ": "𝐐", + "bfR": "𝐑", + "bfS": "𝐒", + "bfT": "𝐓", + "bfU": "𝐔", + "bfV": "𝐕", + "bfW": "𝐖", + "bfX": "𝐗", + "bfY": "𝐘", + "bfZ": "𝐙", + + "bfa": "𝐚", + "bfb": "𝐛", + "bfc": "𝐜", + "bfd": "𝐝", + "bfe": "𝐞", + "bff": "𝐟", + "bfg": "𝐠", + "bfh": "𝐡", + "bfi": "𝐢", + "bfj": "𝐣", + "bfk": "𝐤", + "bfl": "𝐥", + "bfm": "𝐦", + "bfn": "𝐧", + "bfo": "𝐨", + "bfp": "𝐩", + "bfq": "𝐪", + "bfr": "𝐫", + "bfs": "𝐬", + "bft": "𝐭", + "bfu": "𝐮", + "bfv": "𝐯", + "bfw": "𝐰", + "bfx": "𝐱", + "bfy": "𝐲", + "bfz": "𝐳", + + "MiA": "𝐴", + "MiB": "𝐵", + "MiC": "𝐶", + "MiD": "𝐷", + "MiE": "𝐸", + "MiF": "𝐹", + "MiG": "𝐺", + "MiH": "𝐻", + "MiI": "𝐼", + "MiJ": "𝐽", + "MiK": "𝐾", + "MiL": "𝐿", + "MiM": "𝑀", + "MiN": "𝑁", + "MiO": "𝑂", + "MiP": "𝑃", + "MiQ": "𝑄", + "MiR": "𝑅", + "MiS": "𝑆", + "MiT": "𝑇", + "MiU": "𝑈", + "MiV": "𝑉", + "MiW": "𝑊", + "MiX": "𝑋", + "MiY": "𝑌", + "MiZ": "𝑍", + "Mia": "𝑎", + "Mib": "𝑏", + "Mic": "𝑐", + "Mid": "𝑑", + "Mie": "𝑒", + "Mif": "𝑓", + "Mig": "𝑔", + "Mii": "𝑖", + "Mij": "𝑗", + "Mik": "𝑘", + "Mil": "𝑙", + "Mim": "𝑚", + "Min": "𝑛", + "Mio": "𝑜", + "Mip": "𝑝", + "Miq": "𝑞", + "Mir": "𝑟", + "Mis": "𝑠", + "Mit": "𝑡", + "Miu": "𝑢", + "Miv": "𝑣", + "Miw": "𝑤", + "Mix": "𝑥", + "Miy": "𝑦", + "Miz": "𝑧", + "MIA": "𝑨", + "MIB": "𝑩", + "MIC": "𝑪", + "MID": "𝑫", + "MIE": "𝑬", + "MIF": "𝑭", + "MIG": "𝑮", + "MIH": "𝑯", + "MII": "𝑰", + "MIJ": "𝑱", + "MIK": "𝑲", + "MIL": "𝑳", + "MIM": "𝑴", + "MIN": "𝑵", + "MIO": "𝑶", + "MIP": "𝑷", + "MIQ": "𝑸", + "MIR": "𝑹", + "MIS": "𝑺", + "MIT": "𝑻", + "MIU": "𝑼", + "MIV": "𝑽", + "MIW": "𝑾", + "MIX": "𝑿", + "MIY": "𝒀", + "MIZ": "𝒁", + "MIa": "𝒂", + "MIb": "𝒃", + "MIc": "𝒄", + "MId": "𝒅", + "MIe": "𝒆", + "MIf": "𝒇", + "MIg": "𝒈", + "MIh": "𝒉", + "MIi": "𝒊", + "MIj": "𝒋", + "MIk": "𝒌", + "MIl": "𝒍", + "MIm": "𝒎", + "MIn": "𝒏", + "MIo": "𝒐", + "MIp": "𝒑", + "MIq": "𝒒", + "MIr": "𝒓", + "MIs": "𝒔", + "MIt": "𝒕", + "MIu": "𝒖", + "MIv": "𝒗", + "MIw": "𝒘", + "MIx": "𝒙", + "MIy": "𝒚", + "MIz": "𝒛", + "McA": "𝒜", + "McB": "ℬ", + "McC": "𝒞", + "McD": "𝒟", + "McE": "ℰ", + "McF": "ℱ", + "McG": "𝒢", + "McH": "ℋ", + "McI": "ℐ", + "McJ": "𝒥", + "McK": "𝒦", + "McL": "ℒ", + "McM": "ℳ", + "McN": "𝒩", + "McO": "𝒪", + "McP": "𝒫", + "McQ": "𝒬", + "McR": "ℛ", + "McS": "𝒮", + "McT": "𝒯", + "McU": "𝒰", + "McV": "𝒱", + "McW": "𝒲", + "McX": "𝒳", + "McY": "𝒴", + "McZ": "𝒵", + "Mca": "𝒶", + "Mcb": "𝒷", + "Mcc": "𝒸", + "Mcd": "𝒹", + "Mce": "ℯ", + "Mcf": "𝒻", + "Mcg": "ℊ", + "Mch": "𝒽", + "Mci": "𝒾", + "Mcj": "𝒿", + "Mck": "𝓀", + "Mcl": "𝓁", + "Mcm": "𝓂", + "Mcn": "𝓃", + "Mco": "ℴ", + "Mcp": "𝓅", + "Mcq": "𝓆", + "Mcr": "𝓇", + "Mcs": "𝓈", + "Mct": "𝓉", + "Mcu": "𝓊", + "Mcv": "𝓋", + "Mcw": "𝓌", + "Mcx": "𝓍", + "Mcy": "𝓎", + "Mcz": "𝓏", + "MCA": "𝓐", + "MCB": "𝓑", + "MCC": "𝓒", + "MCD": "𝓓", + "MCE": "𝓔", + "MCF": "𝓕", + "MCG": "𝓖", + "MCH": "𝓗", + "MCI": "𝓘", + "MCJ": "𝓙", + "MCK": "𝓚", + "MCL": "𝓛", + "MCM": "𝓜", + "MCN": "𝓝", + "MCO": "𝓞", + "MCP": "𝓟", + "MCQ": "𝓠", + "MCR": "𝓡", + "MCS": "𝓢", + "MCT": "𝓣", + "MCU": "𝓤", + "MCV": "𝓥", + "MCW": "𝓦", + "MCX": "𝓧", + "MCY": "𝓨", + "MCZ": "𝓩", + "MCa": "𝓪", + "MCb": "𝓫", + "MCc": "𝓬", + "MCd": "𝓭", + "MCe": "𝓮", + "MCf": "𝓯", + "MCg": "𝓰", + "MCh": "𝓱", + "MCi": "𝓲", + "MCj": "𝓳", + "MCk": "𝓴", + "MCl": "𝓵", + "MCm": "𝓶", + "MCn": "𝓷", + "MCo": "𝓸", + "MCp": "𝓹", + "MCq": "𝓺", + "MCr": "𝓻", + "MCs": "𝓼", + "MCt": "𝓽", + "MCu": "𝓾", + "MCv": "𝓿", + "MCw": "𝔀", + "MCx": "𝔁", + "MCy": "𝔂", + "MCz": "𝔃", + "MfA": "𝔄", + "MfB": "𝔅", + "MfC": "ℭ", + "MfD": "𝔇", + "MfE": "𝔈", + "MfF": "𝔉", + "MfG": "𝔊", + "MfH": "ℌ", + "MfI": "ℑ", + "MfJ": "𝔍", + "MfK": "𝔎", + "MfL": "𝔏", + "MfM": "𝔐", + "MfN": "𝔑", + "MfO": "𝔒", + "MfP": "𝔓", + "MfQ": "𝔔", + "MfR": "ℜ", + "MfS": "𝔖", + "MfT": "𝔗", + "MfU": "𝔘", + "MfV": "𝔙", + "MfW": "𝔚", + "MfX": "𝔛", + "MfY": "𝔜", + "MfZ": "ℨ", + "Mfa": "𝔞", + "Mfb": "𝔟", + "Mfc": "𝔠", + "Mfd": "𝔡", + "Mfe": "𝔢", + "Mff": "𝔣", + "Mfg": "𝔤", + "Mfh": "𝔥", + "Mfi": "𝔦", + "Mfj": "𝔧", + "Mfk": "𝔨", + "Mfl": "𝔩", + "Mfm": "𝔪", + "Mfn": "𝔫", + "Mfo": "𝔬", + "Mfp": "𝔭", + "Mfq": "𝔮", + "Mfr": "𝔯", + "Mfs": "𝔰", + "Mft": "𝔱", + "Mfu": "𝔲", + "Mfv": "𝔳", + "Mfw": "𝔴", + "Mfx": "𝔵", + "Mfy": "𝔶", + "Mfz": "𝔷", + + "yen": "¥", + "varrho": "ϱ", + "varkappa": "ϰ", + "varkai": "ϗ", + "varnothing": "∅", + "varpi": "ϖ", + "varphi": "ϕ", + "varprime": "′", + "varpropto": "∝", + "vartheta": "ϑ", + "vartriangleleft": "⊲", + "vartriangleright": "⊳", + "varbeta": "ϐ", + "varsigma": "ς", + "veebar": "⊻", + "vee": "∨", + "ve": "ě", + "vE": "Ě", + "vdash": "⊢", + "vdots": "⋮", + "vd": "ď", + "vDash": "⊨", + "vD": "Ď", + "vc": "č", + "vC": "Č", + "koppa": "ϟ", + "kip": "₭", + "ki": "į", + "kI": "Į", + "kelvin": "K", + "kappa": "κ", + "khei": "ϧ", + "warning": "⚠", + "won": "₩", + "wedge": "∧", + "wp": "℘", + "wr": "≀", + "Dei": "Ϯ", + "Delta": "Δ", + "Digamma": "Ϝ", + "Diamond": "◇", + "Downarrow": "⇓", + "DH": "Ð", + "zeta": "ζ", + "Eta": "Η", + "Epsilon": "Ε", + "Beta": "Β", + "Box": "□", + "Bumpeq": "≎", + + "bbA": "𝔸", + "bbB": "𝔹", + "bbC": "ℂ", + "bbD": "𝔻", + "bbE": "𝔼", + "bbF": "𝔽", + "bbG": "𝔾", + "bbH": "ℍ", + "bbI": "𝕀", + "bbJ": "𝕁", + "bbK": "𝕂", + "bbL": "𝕃", + "bbM": "𝕄", + "bbN": "ℕ", + "bbO": "𝕆", + "bbP": "ℙ", + "bbQ": "ℚ", + "bbR": "ℝ", + "bbS": "𝕊", + "bbT": "𝕋", + "bbU": "𝕌", + "bbV": "𝕍", + "bbW": "𝕎", + "bbX": "𝕏", + "bbY": "𝕐", + "bbZ": "ℤ", + "bba": "𝕒", + "bbb": "𝕓", + "bbc": "𝕔", + "bbd": "𝕕", + "bbe": "𝕖", + "bbf": "𝕗", + "bbg": "𝕘", + "bbh": "𝕙", + "bbi": "𝕚", + "bbj": "𝕛", + "bbk": "𝕜", + "bbl": "𝕝", + "bbm": "𝕞", + "bbn": "𝕟", + "bbo": "𝕠", + "bbp": "𝕡", + "bbq": "𝕢", + "bbr": "𝕣", + "bbs": "𝕤", + "bbt": "𝕥", + "bbu": "𝕦", + "bbv": "𝕧", + "bbw": "𝕨", + "bbx": "𝕩", + "bby": "𝕪", + "bbz": "𝕫", + + "Rge0": "ℝ≥0", + "R>=0": "ℝ≥0", + "nnreal": "ℝ≥0", + "ennreal": "ℝ≥0∞", + "enat": "ℕ∞", + "Zsqrt": "ℤ√", + "zsqrtd": "ℤ√", + "liel": "⁅", + "bracketl": "⁅", + "lier": "⁆", + "[-": "⁅", + "-]": "⁆", + "bracketr": "⁆", + "nhds": "𝓝", + "nbhds": "𝓝", + "X": "⨯", + "vectorproduct": "⨯", + "crossproduct": "⨯", + "coprod": "⨿", + "sigmaobj": "∐", + "xf": "×ᶠ", + "exf": "∃ᶠ", + "c[": "⦃", + "c]": "⦄", + "Yot": "Ϳ", + "goal": "⊢", + "Vdash": "⊩", + "Vert": "‖", + "Vvdash": "⊪" +} diff --git a/client/src/monaco-lean4/abbreviation/config.ts b/client/src/monaco-lean4/abbreviation/config.ts new file mode 100644 index 00000000..3f03146b --- /dev/null +++ b/client/src/monaco-lean4/abbreviation/config.ts @@ -0,0 +1,30 @@ +import { serializerWithDefault, VsCodeSetting } from '../utils/VsCodeSetting' + +/** + * Exposes (observable) settings for the abbreviation feature. + */ +export class AbbreviationConfig { + readonly inputModeEnabled = new VsCodeSetting('lean4.input.enabled', { + serializer: serializerWithDefault(true), + }) + + readonly abbreviationCharacter = new VsCodeSetting('lean4.input.leader', { + serializer: serializerWithDefault('\\'), + }) + + readonly languages = new VsCodeSetting('lean4.input.languages', { + serializer: serializerWithDefault(['lean4']), + }) + + readonly inputModeCustomTranslations = new VsCodeSetting('lean4.input.customTranslations', { + serializer: serializerWithDefault({}), + }) + + readonly eagerReplacementEnabled = new VsCodeSetting('lean4.input.eagerReplacementEnabled', { + serializer: serializerWithDefault(true), + }) +} + +export interface SymbolsByAbbreviation { + [abbrev: string]: string +} diff --git a/client/src/monaco-lean4/abbreviation/index.ts b/client/src/monaco-lean4/abbreviation/index.ts new file mode 100644 index 00000000..c7a1dac1 --- /dev/null +++ b/client/src/monaco-lean4/abbreviation/index.ts @@ -0,0 +1,34 @@ +import { Disposable, languages } from 'vscode' +import { autorunDisposable } from '../utils/autorunDisposable' +import { AbbreviationHoverProvider } from './AbbreviationHoverProvider' +import { AbbreviationProvider } from './AbbreviationProvider' +import { AbbreviationConfig } from './config' +import { AbbreviationRewriterFeature } from './rewriter/AbbreviationRewriterFeature' + +export class AbbreviationFeature { + private readonly disposables = new Array() + readonly abbreviations: AbbreviationProvider + + constructor() { + const config = new AbbreviationConfig() + this.abbreviations = new AbbreviationProvider(config) + + this.disposables.push( + autorunDisposable(disposables => { + disposables.push( + languages.registerHoverProvider( + config.languages.get(), + new AbbreviationHoverProvider(config, this.abbreviations), + ), + ) + }), + new AbbreviationRewriterFeature(config, this.abbreviations), + ) + } + + dispose(): void { + for (const d of this.disposables) { + d.dispose() + } + } +} diff --git a/client/src/monaco-lean4/abbreviation/rewriter/AbbreviationRewriter.ts b/client/src/monaco-lean4/abbreviation/rewriter/AbbreviationRewriter.ts new file mode 100644 index 00000000..7edc0873 --- /dev/null +++ b/client/src/monaco-lean4/abbreviation/rewriter/AbbreviationRewriter.ts @@ -0,0 +1,329 @@ +import { + commands, + Disposable, + extensions, + OutputChannel, + Range as LineColRange, + Selection, + TextDocument, + TextEditor, + window, + workspace, +} from 'vscode' +import { assert } from '../../utils/assert' +import { AbbreviationProvider } from '../AbbreviationProvider' +import { AbbreviationConfig } from '../config' +import { Range } from './Range' +import { TrackedAbbreviation } from './TrackedAbbreviation' + +/** + * Tracks abbreviations in a given text editor and replaces them when dynamically. + */ +export class AbbreviationRewriter { + private readonly disposables = new Array() + /** + * All tracked abbreviations are disjoint. + */ + private readonly trackedAbbreviations = new Set() + private readonly decorationType = window.createTextEditorDecorationType({ + textDecoration: 'underline', + }) + + private dontTrackNewAbbr = false + private stderrOutput: OutputChannel + private firstOutput = true + private isVimExtensionInstalled = false + + private checkIsVimExtensionInstalled() { + this.isVimExtensionInstalled = extensions.getExtension('vscodevim.vim') !== undefined + } + + constructor( + private readonly config: AbbreviationConfig, + private readonly abbreviationProvider: AbbreviationProvider, + private readonly textEditor: TextEditor, + ) { + this.disposables.push(this.decorationType) + + this.disposables.push( + workspace.onDidChangeTextDocument(e => { + if (e.document !== this.textEditor.document) { + return + } + + const changes = e.contentChanges.slice(0) + // We need to process the changes at the bottom first. + // Otherwise, changes at the top will move spans at the bottom down. + changes.sort((c1, c2) => c2.rangeOffset - c1.rangeOffset) + + for (const c of changes) { + const range = new Range(c.rangeOffset, c.rangeLength) + this.processChange(range, c.text) + } + + this.updateState() + + // Replace any tracked abbreviation that is either finished or unique. + void this.forceReplace( + [...this.trackedAbbreviations].filter( + abbr => + abbr.finished || + (this.config.eagerReplacementEnabled.get() && abbr.isAbbreviationUniqueAndComplete), + ), + ) + }), + ) + this.disposables.push( + window.onDidChangeTextEditorSelection(e => { + if (e.textEditor.document !== this.textEditor.document) { + return + } + + // Replace any tracked abbreviation that lost selection. + void this.forceReplace( + [...this.trackedAbbreviations].filter( + abbr => + !e.selections.some(s => + abbr.range.containsRange(fromVsCodeRange(s, e.textEditor.document).withLength(0)), + ), + ), + ) + }), + ) + + this.disposables.push( + commands.registerTextEditorCommand('lean4.input.convert', async () => + this.forceReplace([...this.trackedAbbreviations]), + ), + ) + + this.checkIsVimExtensionInstalled() + this.disposables.push(extensions.onDidChange(_ => this.checkIsVimExtensionInstalled())) + } + + private writeError(e: string) { + this.stderrOutput = this.stderrOutput || window.createOutputChannel('Lean: Editor') + this.stderrOutput.appendLine(e) + if (this.firstOutput) { + this.stderrOutput.show(true) + this.firstOutput = false + } + } + + private async forceReplace(abbreviations: TrackedAbbreviation[]): Promise { + if (abbreviations.length === 0) { + return + } + for (const a of abbreviations) { + this.trackedAbbreviations.delete(a) + } + + const replacements = this.computeReplacements(abbreviations) + const replacingSuccessful = await this.replaceAbbreviations(replacements) + + if (replacingSuccessful) { + this.moveSelections(replacements) + this.abbreviationProvider.onAbbreviationsCompleted(this.textEditor) + } else { + // If replacing the abbreviation did not succeed, keep it around so that we can re-try next time + // when the text document was changed, the cursor was moved around or the replacement was triggered + // manually. + for (const a of abbreviations) { + this.trackedAbbreviations.add(a) + } + } + + this.updateState() + } + + private computeReplacements(abbreviations: TrackedAbbreviation[]): { + range: Range + newText: string + cursorOffset?: number | undefined + }[] { + const cursorVar = '$CURSOR' + const replacements = new Array<{ + range: Range + newText: string + cursorOffset?: number | undefined + }>() + + for (const abbr of abbreviations) { + const symbol = abbr.matchingSymbol + if (symbol) { + const newText = symbol.replace(cursorVar, '') + let cursorOffset: number | undefined = symbol.indexOf(cursorVar) + if (cursorOffset === -1) { + cursorOffset = undefined + } + replacements.push({ + range: abbr.range, + newText, + cursorOffset, + }) + } + } + + return replacements + } + + private async replaceAbbreviations( + replacements: { + range: Range + newText: string + cursorOffset?: number | undefined + }[], + ): Promise { + // We don't want replaced symbols (e.g. "\") to trigger abbreviations. + this.dontTrackNewAbbr = true + + let ok = false + let retries = 0 + try { + // The user may have changed the text document in-between `this.textEditor` being updated + // (when the call to the extension was started) and `this.textEditor.edit()` being executed. + // In this case, since the state of the editor that the extension sees and the state that + // the user sees are different, VS Code will reject the edit. + // This occurs especially often in setups with increased latency until the extension is triggered, + // e.g. an SSH setup. Since VS Code does not appear to support an atomic read -> write operation, + // unfortunately the only thing we can do here is to retry. + while (!ok && retries < 10) { + ok = await this.textEditor.edit(builder => { + for (const r of replacements) { + builder.replace(toVsCodeRange(r.range, this.textEditor.document), r.newText) + } + }) + retries++ + } + } catch (e) { + this.writeError('Error while replacing abbreviation: ' + e) + } + + this.dontTrackNewAbbr = false + + return ok + } + + private moveSelections( + replacements: { + range: Range + newText: string + cursorOffset?: number | undefined + }[], + ) { + // Only move the cursor if there were any abbreviations with $CURSOR. + // This is important because setting `this.textEditor.selections = this.textEditor.selections` + // may override changes to the cursor made between the `this.textEditor.edit` call and updating + // the selection. This is due to `this.textEditor.selections` being only updated on `await`. + // + // When users have the Vim extension installed, the builtin selection manipulation of VS Code + // consistently moves the cursor to a wrong position, likely because the Vim extension manipulates + // the cursor itself or because edits sent by the VS Code extension conflict with that of the + // AbbreviationRewriter. In this case, we fall back to manually manipulating the cursor. This is + // subject to race conditions, but at least not consistently wrong, as would otherwise be the case + // with the Vim extension installed. + if (!replacements.some(r => r.cursorOffset) && !this.isVimExtensionInstalled) { + return + } + + // Process replacements with lowest offset first + replacements.sort((a, b) => a.range.offset - b.range.offset) + + const afterEditReplacements = new Array<{ + range: Range + newText: string + cursorOffset?: number | undefined + }>() + let totalOffsetShift = 0 + for (const r of replacements) { + // Re-adjust range to account for new length and changes in prior lengths. + const afterEditRange = new Range(r.range.offset + totalOffsetShift, r.newText.length) + afterEditReplacements.push({ + range: afterEditRange, + newText: r.newText, + cursorOffset: r.cursorOffset, + }) + totalOffsetShift += r.newText.length - r.range.length + } + + const newSelections = this.textEditor.selections + .map(s => fromVsCodeRange(s, this.textEditor.document)) + .map(s => { + for (const r of afterEditReplacements) { + if (!r.cursorOffset) { + // Only move cursor if abbreviation contained $CURSOR + continue + } + + const isCursorAtEndOfAbbreviation = s.offset === r.range.offsetEnd + 1 + // Safety check: Prevents moving the cursor if e.g. the replacement triggered + // because the selection was moved away from the abbreviation. + if (isCursorAtEndOfAbbreviation) { + // Move cursor backwards to the position of $CURSOR + return s.move(r.cursorOffset - r.newText.length) + } + } + + // Cursor not at the end of any abbreviation that contained $CURSOR + // => Keep it where it is + return s + }) + + this.textEditor.selections = newSelections.map(s => { + const vr = toVsCodeRange(s, this.textEditor.document) + return new Selection(vr.start, vr.end) + }) + } + + private updateState() { + this.textEditor.setDecorations( + this.decorationType, + [...this.trackedAbbreviations].map(a => toVsCodeRange(a.range, this.textEditor.document)), + ) + + void this.setInputActive(this.trackedAbbreviations.size > 0) + } + + private async setInputActive(isActive: boolean) { + await commands.executeCommand('setContext', 'lean4.input.isActive', isActive) + } + + private processChange(range: Range, text: string): { affectedAbbr: TrackedAbbreviation | undefined } { + let affectedAbbr: TrackedAbbreviation | undefined + for (const abbr of [...this.trackedAbbreviations]) { + const { isAffected, shouldStopTracking } = abbr.processChange(range, text) + if (isAffected) { + // At most one abbreviation should be affected + assert(() => !affectedAbbr) + affectedAbbr = abbr + } + if (shouldStopTracking) { + this.trackedAbbreviations.delete(abbr) + } + } + + if (text === this.config.abbreviationCharacter.get() && !affectedAbbr && !this.dontTrackNewAbbr) { + const abbr = new TrackedAbbreviation(new Range(range.offset + 1, 0), '', this.abbreviationProvider) + this.trackedAbbreviations.add(abbr) + } + return { affectedAbbr } + } + + dispose(): void { + for (const d of this.disposables) { + d.dispose() + } + } +} + +function fromVsCodeRange(range: LineColRange, doc: TextDocument): Range { + const start = doc.offsetAt(range.start) + const end = doc.offsetAt(range.end) + return new Range(start, end - start) +} + +function toVsCodeRange(range: Range, doc: TextDocument): LineColRange { + const start = doc.positionAt(range.offset) + const end = doc.positionAt(range.offsetEnd + 1) + return new LineColRange(start, end) +} diff --git a/client/src/monaco-lean4/abbreviation/rewriter/AbbreviationRewriterFeature.ts b/client/src/monaco-lean4/abbreviation/rewriter/AbbreviationRewriterFeature.ts new file mode 100644 index 00000000..af77e795 --- /dev/null +++ b/client/src/monaco-lean4/abbreviation/rewriter/AbbreviationRewriterFeature.ts @@ -0,0 +1,54 @@ +import { observable } from 'mobx' +import { Disposable, languages, TextEditor, window } from 'vscode' +import { autorunDisposable } from '../../utils/autorunDisposable' +import { AbbreviationProvider } from '../AbbreviationProvider' +import { AbbreviationConfig } from '../config' +import { AbbreviationRewriter } from './AbbreviationRewriter' + +/** + * Sets up everything required for the abbreviation rewriter feature. + * Creates an `AbbreviationRewriter` for the active editor. + */ +export class AbbreviationRewriterFeature { + private readonly disposables = new Array() + + @observable + private activeTextEditor: TextEditor | undefined + + constructor( + private readonly config: AbbreviationConfig, + abbreviationProvider: AbbreviationProvider, + ) { + this.activeTextEditor = window.activeTextEditor + + this.disposables.push( + window.onDidChangeActiveTextEditor(e => { + this.activeTextEditor = e + }), + autorunDisposable(disposables => { + if (this.activeTextEditor && this.shouldEnableRewriterForEditor(this.activeTextEditor)) { + // This creates an abbreviation rewriter for the active text editor. + // Old rewriters are disposed automatically. + // This is also updated when this feature is turned off/on. + disposables.push(new AbbreviationRewriter(config, abbreviationProvider, this.activeTextEditor)) + } + }), + ) + } + + private shouldEnableRewriterForEditor(editor: TextEditor): boolean { + if (!this.config.inputModeEnabled.get()) { + return false + } + if (!languages.match(this.config.languages.get(), editor.document)) { + return false + } + return true + } + + dispose(): void { + for (const d of this.disposables) { + d.dispose() + } + } +} diff --git a/client/src/monaco-lean4/abbreviation/rewriter/Range.ts b/client/src/monaco-lean4/abbreviation/rewriter/Range.ts new file mode 100644 index 00000000..9ec49176 --- /dev/null +++ b/client/src/monaco-lean4/abbreviation/rewriter/Range.ts @@ -0,0 +1,95 @@ +import { assert } from '../../utils/assert' + +/** + * A general purpose range implementation. + * Is offset/length based in contrast to `vscode.Range` which is line/column based. + */ +export class Range { + constructor( + readonly offset: number, + readonly length: number, + ) { + assert(() => length >= 0) + } + + contains(offset: number): boolean { + return this.offset <= offset && offset <= this.offsetEnd + } + + get offsetEnd(): number { + return this.offset + this.length - 1 + } + + get isEmpty(): boolean { + return this.length === 0 + } + + toString(): string { + return `[${this.offset}, +${this.length})` + } + + move(delta: number): Range { + return new Range(this.offset + delta, this.length) + } + + moveKeepEnd(delta: number): Range { + assert(() => delta <= this.length) + const result = new Range(this.offset + delta, this.length - delta) + assert(() => result.offsetEnd === this.offsetEnd) + return result + } + + moveEnd(delta: number): Range { + return new Range(this.offset, this.length + delta) + } + + withLength(newLength: number): Range { + return new Range(this.offset, newLength) + } + + containsRange(other: Range): boolean { + /* + * 0 1 2 3 4 5 + * |# # # this { offset: 1, end: 3, len: 3 } + * | | other: false { offset: 0, end: -1, len: 0 } + * | | | | other: true { offset: i, end: i - 1, len: 0 } + * |# |# |# other: true + * |# # |# # other: false + * |# # # other: true + */ + // If other is non-empty, this must contain all its points. + + return this.offset <= other.offset && other.offsetEnd <= this.offsetEnd + } + + /** + * Check whether this range if after `range`. + */ + isAfter(range: Range): boolean { + /* + * 0 1 2 3 4 5 + * |# # # this + * | | other: true + * |# other: true + * |# other: false + * |# # other: false + */ + return range.offsetEnd < this.offset + } + + /** + * Check whether this range if before `range`. + */ + isBefore(range: Range): boolean { + /* + * 0 1 2 3 4 5 + * |# # # this + * | | other: true + * |# other: true + * |# other: false + * | other: false + * |# # other: false + */ + return range.offset > this.offsetEnd + } +} diff --git a/client/src/monaco-lean4/abbreviation/rewriter/TrackedAbbreviation.ts b/client/src/monaco-lean4/abbreviation/rewriter/TrackedAbbreviation.ts new file mode 100644 index 00000000..461d9498 --- /dev/null +++ b/client/src/monaco-lean4/abbreviation/rewriter/TrackedAbbreviation.ts @@ -0,0 +1,90 @@ +import { AbbreviationProvider } from '../AbbreviationProvider' +import { Range } from './Range' + +/** + * Represents an abbreviation that is tracked and currently typed by the user. + * When the multi-cursor feature is used, multiple abbreviations can be tracked at once. + */ +export class TrackedAbbreviation { + private _abbreviationRange: Range + + get abbreviationRange(): Range { + return this._abbreviationRange + } + + get range(): Range { + return this.abbreviationRange.moveKeepEnd(-1) + } + + get abbreviation(): string { + return this._text + } + + get matchingSymbol(): string | undefined { + return this.abbreviationProvider.getReplacementText(this.abbreviation) + } + + /** + * Does this abbreviation uniquely identify a symbol and is it complete? + */ + get isAbbreviationUniqueAndComplete(): boolean { + return ( + this.abbreviationProvider.findSymbolsByAbbreviationPrefix(this.abbreviation).length === 1 && + !!this.abbreviationProvider.getSymbolForAbbreviation(this.abbreviation) + ) + } + + private _finished = false + /** + * Indicates whether this abbreviation has been continued with non-abbreviation characters. + * Such abbreviations should be replaced immediately. + */ + get finished(): boolean { + return this._finished + } + + constructor( + abbreviationRange: Range, + private _text: string, + private readonly abbreviationProvider: AbbreviationProvider, + ) { + this._abbreviationRange = abbreviationRange + } + + processChange(range: Range, newText: string): { shouldStopTracking: boolean; isAffected: boolean } { + if (this.abbreviationRange.containsRange(range)) { + this._finished = false + + if (this.abbreviationRange.isBefore(range)) { + // `newText` is appended to `this.abbreviation` + if ( + this.abbreviationProvider.findSymbolsByAbbreviationPrefix(this.abbreviation + newText).length === 0 + ) { + // newText is not helpful anymore. Finish this and don't accept the change. + this._finished = true + return { + shouldStopTracking: false, + isAffected: false, + } + } + } + + this._abbreviationRange = this.abbreviationRange.moveEnd(newText.length - range.length) + const startStr = this.abbreviation.substr(0, range.offset - this.abbreviationRange.offset) + const endStr = this.abbreviation.substr(range.offsetEnd + 1 - this.abbreviationRange.offset) + this._text = startStr + newText + endStr + + return { shouldStopTracking: false, isAffected: true } + } else if (range.isBefore(this.range)) { + // The changed happened before us. We need to move. + this._abbreviationRange = this._abbreviationRange.move(newText.length - range.length) + return { shouldStopTracking: false, isAffected: false } + } else if (range.isAfter(this.range)) { + // The change does not affect us. + return { shouldStopTracking: false, isAffected: false } + } else { + // We cannot process the change. Abort tracking. + return { shouldStopTracking: true, isAffected: false } + } + } +} diff --git a/client/src/monaco-lean4/config.ts b/client/src/monaco-lean4/config.ts new file mode 100644 index 00000000..33912261 --- /dev/null +++ b/client/src/monaco-lean4/config.ts @@ -0,0 +1,294 @@ +import * as fs from 'fs' +import * as path from 'path' +import { workspace } from 'vscode' +import { logger } from './utils/logger' + +// TODO: does currently not contain config options for `./abbreviation` +// so that it is easy to keep it in sync with vscode-lean. + +export function getEnvPath(): string { + if (process.platform === 'win32') { + return process.env.Path ?? '' + } else { + return process.env.PATH ?? '' + } +} + +export function setEnvPath(value: string): void { + if (process.platform === 'win32') { + process.env.Path = value + } else { + process.env.PATH = value + } +} + +function splitEnvPath(value: string): string[] { + return value.split(path.delimiter) +} + +function joinEnvPath(value: string[]): string { + return value.join(path.delimiter) +} + +// Make a copy of the passed process environment that includes the user's +// `lean4.serverEnvPaths` in the path key, and adds the key/value pairs from +// `lean4.serverEnv`. Both of these settings can be found in the user's +// settings.json file +export function addServerEnvPaths(input_env: NodeJS.ProcessEnv): NodeJS.ProcessEnv { + const env = Object.assign({}, input_env, serverEnv()) + const paths = serverEnvPaths() + if (paths.length !== 0) { + setEnvPath(joinEnvPath(paths) + path.delimiter + getEnvPath()) + } + return env +} + +export function getDefaultElanPath(): string { + let elanPath = '' + if (process.platform === 'win32') { + elanPath = process.env.USERPROFILE + '\\.elan\\bin' + } else { + elanPath = process.env.HOME + '/.elan/bin' + } + return elanPath +} + +export function addDefaultElanPath(): void { + const paths = getEnvPath() + const elanPath = getDefaultElanPath() + if (paths.indexOf(elanPath) < 0) { + setEnvPath(paths + path.delimiter + elanPath) + } +} + +function findToolchainBin(root: string): string { + logger.log(`Looking for toolchains in ${root}`) + if (!fs.existsSync(root)) { + return '' + } + const toolchains = fs.readdirSync(path.join(root, '..', 'toolchains')) + for (const toolchain of toolchains) { + if (toolchain.indexOf('leanprover--lean4') >= 0) { + return path.join(root, '..', 'toolchains', toolchains[0], 'bin') + } + } + return '' +} + +export function addToolchainBinPath(elanPath: string) { + const bin = findToolchainBin(elanPath) + if (bin) { + const paths = getEnvPath() + setEnvPath(paths + path.delimiter + bin) + } +} + +export function findProgramInPath(name: string): string { + if (fs.existsSync(name)) { + return name + } + const extensions: string[] = [] + if (process.platform === 'win32') { + extensions.push('.exe') + extensions.push('.com') + extensions.push('.cmd') + } else { + extensions.push('') + } + const parts = splitEnvPath(getEnvPath()) + for (const part of parts) { + for (const ext of extensions) { + const fullPath = path.join(part, name + ext) + if (fs.existsSync(fullPath)) { + return fullPath + } + } + } + return '' +} + +export function removeElanPath(): string { + const parts = splitEnvPath(getEnvPath()) + let result = '' + for (let i = 0; i < parts.length; ) { + const part = parts[i] + if (part.indexOf('.elan') > 0) { + logger.log(`removing path to elan: ${part}`) + result = part + parts.splice(i, 1) + } else { + i++ + } + } + + setEnvPath(joinEnvPath(parts)) + return result +} + +export function getPowerShellPath(): string { + const windir = process.env.windir + return `${windir}\\System32\\WindowsPowerShell\\v1.0\\powershell.exe` +} + +export function toolchainPath(): string { + return workspace.getConfiguration('lean4').get('toolchainPath', '') +} + +export function lakePath(): string { + return workspace.getConfiguration('lean4').get('lakePath', '') +} + +export function lakeEnabled(): boolean { + return workspace.getConfiguration('lean4').get('enableLake', false) +} + +export function serverEnv(): object { + return workspace.getConfiguration('lean4').get('serverEnv', {}) +} + +export function automaticallyBuildDependencies(): boolean { + return workspace.getConfiguration('lean4').get('automaticallyBuildDependencies', false) +} + +export function serverEnvPaths(): string[] { + return workspace.getConfiguration('lean4').get('serverEnvPaths', []) +} + +export function serverArgs(): string[] { + return workspace.getConfiguration('lean4').get('serverArgs', []) +} + +export function serverLoggingEnabled(): boolean { + return workspace.getConfiguration('lean4.serverLogging').get('enabled', false) +} + +export function serverLoggingPath(): string { + return workspace.getConfiguration('lean4.serverLogging').get('path', '.') +} + +export function shouldAutofocusOutput(): boolean { + return workspace.getConfiguration('lean4').get('autofocusOutput', false) +} + +export function getInfoViewStyle(): string { + const val = workspace.getConfiguration('lean4.infoview').get('style') + if (val !== undefined) return val + // Try deprecated name of the same setting if not found + return workspace.getConfiguration('lean4').get('infoViewStyle', '') +} + +export function getInfoViewAutoOpen(): boolean { + const val = workspace.getConfiguration('lean4.infoview').get('autoOpen') + if (val !== undefined) return val + return workspace.getConfiguration('lean4').get('infoViewAutoOpen', true) +} + +export function getInfoViewAutoOpenShowsGoal(): boolean { + const val = workspace.getConfiguration('lean4.infoview').get('autoOpenShowsGoal') + if (val !== undefined) return val + return workspace.getConfiguration('lean4').get('infoViewAutoOpenShowGoal', true) +} + +export function getInfoViewAllErrorsOnLine(): boolean { + const val = workspace.getConfiguration('lean4.infoview').get('allErrorsOnLine') + if (val !== undefined) return val + return workspace.getConfiguration('lean4').get('infoViewAllErrorsOnLine', true) +} + +export function getInfoViewDebounceTime(): number { + return workspace.getConfiguration('lean4.infoview').get('debounceTime', 50) +} + +export function getInfoViewShowExpectedType(): boolean { + return workspace.getConfiguration('lean4.infoview').get('showExpectedType', true) +} + +export function getInfoViewShowGoalNames(): boolean { + return workspace.getConfiguration('lean4.infoview').get('showGoalNames', true) +} + +export function getInfoViewEmphasizeFirstGoal(): boolean { + return workspace.getConfiguration('lean4.infoview').get('emphasizeFirstGoal', false) +} + +export function getInfoViewReverseTacticState(): boolean { + return workspace.getConfiguration('lean4.infoview').get('reverseTacticState', false) +} + +export function getInfoViewShowTooltipOnHover(): boolean { + return workspace.getConfiguration('lean4.infoview').get('showTooltipOnHover', true) +} + +export function getElaborationDelay(): number { + return workspace.getConfiguration('lean4').get('elaborationDelay', 200) +} + +export function shouldShowInvalidProjectWarnings(): boolean { + return workspace.getConfiguration('lean4').get('showInvalidProjectWarnings', true) +} + +export function getFallBackToStringOccurrenceHighlighting(): boolean { + return workspace.getConfiguration('lean4').get('fallBackToStringOccurrenceHighlighting', false) +} + +export function getLeanExecutableName(): string { + if (process.platform === 'win32') { + return 'lean.exe' + } + return 'lean' +} + +export function isRunningTest(): boolean { + return typeof process.env.LEAN4_TEST_FOLDER === 'string' +} + +export function getTestFolder(): string { + return typeof process.env.LEAN4_TEST_FOLDER === 'string' ? process.env.LEAN4_TEST_FOLDER : '' +} + +export function getDefaultLeanVersion(): string { + return typeof process.env.DEFAULT_LEAN_TOOLCHAIN === 'string' + ? process.env.DEFAULT_LEAN_TOOLCHAIN + : 'leanprover/lean4:stable' +} + +export function isElanDisabled(): boolean { + return typeof process.env.DISABLE_ELAN === 'string' +} + +/** The editor line height, in pixels. */ +export function getEditorLineHeight(): number { + // The implementation + // (recommended by Microsoft: https://github.com/microsoft/vscode/issues/125341#issuecomment-854812591) + // is absolutely cursed. It's just to copy whatever VSCode does internally. + const fontSize = workspace.getConfiguration('editor').get('fontSize') ?? 0 + let lineHeight = workspace.getConfiguration('editor').get('lineHeight') ?? 0 + + const GOLDEN_LINE_HEIGHT_RATIO = process.platform === 'darwin' ? 1.5 : 1.35 + const MINIMUM_LINE_HEIGHT = 8 + + if (lineHeight === 0) { + lineHeight = GOLDEN_LINE_HEIGHT_RATIO * fontSize + } else if (lineHeight < MINIMUM_LINE_HEIGHT) { + // Values too small to be line heights in pixels are in ems. + lineHeight = lineHeight * fontSize + } + + // Enforce integer, minimum constraints + lineHeight = Math.round(lineHeight) + if (lineHeight < MINIMUM_LINE_HEIGHT) { + lineHeight = MINIMUM_LINE_HEIGHT + } + + return lineHeight +} + +/** + * The literal 'production' or 'development', depending on the build. + * Should be turned into a string literal by build tools. + */ +export const prodOrDev: string = + process.env.NODE_ENV && process.env.NODE_ENV === 'production' ? 'production' : 'development' + +/** The literal '.min' or empty, depending on the build. See {@link prodOrDev}. */ +export const minIfProd: string = process.env.NODE_ENV && process.env.NODE_ENV === 'production' ? '.min' : '' diff --git a/client/src/monaco-lean4/docview.ts b/client/src/monaco-lean4/docview.ts new file mode 100644 index 00000000..b702f9ed --- /dev/null +++ b/client/src/monaco-lean4/docview.ts @@ -0,0 +1,428 @@ +/* eslint-disable @typescript-eslint/no-unsafe-assignment */ +import axios from 'axios' +import { extname } from 'path' +import { URL } from 'url' +import { + commands, + Disposable, + languages, + Position, + Range, + TextDocument, + Uri, + ViewColumn, + WebviewOptions, + WebviewPanel, + WebviewPanelOptions, + window, + workspace, +} from 'vscode' +import { AbbreviationConfig, SymbolsByAbbreviation } from './abbreviation/config' +import { TempFolder } from './utils/tempFolder' +import cheerio = require('cheerio') + +export function mkCommandUri(commandName: string, ...args: any[]): string { + return `command:${commandName}?${encodeURIComponent(JSON.stringify(args))}` +} + +function createLocalFileUrl(path: string) { + const re = /\\/g + return `file:${path}`.replace(re, '/') +} + +export class DocViewProvider implements Disposable { + private subscriptions: Disposable[] = [] + private currentURL: string | undefined = undefined + private backStack: string[] = [] + private forwardStack: string[] = [] + private tempFolder: TempFolder + private abbreviations: SymbolsByAbbreviation + private extensionUri: Uri + private tryItDoc: TextDocument | null = null + private html: string = '' + + constructor(extensionUri: Uri) { + this.extensionUri = extensionUri + this.subscriptions.push( + commands.registerCommand('lean4.docView.open', () => this.open()), + commands.registerCommand('lean4.docView.openUrl', (url: string) => this.open(url)), + commands.registerCommand('lean4.docView.back', () => this.back()), + commands.registerCommand('lean4.docView.forward', () => this.forward()), + commands.registerCommand('lean4.docView.openTryIt', (code: string) => this.tryIt(code)), + commands.registerCommand('lean4.docView.openExample', (file: string) => this.example(file)), + commands.registerCommand('lean4.docView.showAllAbbreviations', () => this.showAbbreviations()), + ) + this.subscriptions.push( + workspace.onDidCloseTextDocument(doc => { + if (doc === this.tryItDoc) { + this.tryItDoc = null + } + }), + ) + } + + private getTempFolder(): TempFolder { + if (!this.tempFolder) { + this.tempFolder = new TempFolder('lean4') + this.subscriptions.push(this.tempFolder) + } + return this.tempFolder + } + + setAbbreviations(abbrev: SymbolsByAbbreviation): void { + this.abbreviations = abbrev + } + + private async tryIt(code: string) { + let replace = false + if (this.tryItDoc == null) { + this.tryItDoc = await workspace.openTextDocument({ language: 'lean4', content: code }) + } else { + // reuse the editor that is already open so we don't end up with a million tabs. + replace = true + } + const editor = await window.showTextDocument(this.tryItDoc, ViewColumn.One) + if (replace && editor) { + await editor.edit(edit => { + // append the new code to the end of the document. + const end = new Position(editor.document.lineCount, 0) + edit.replace(new Range(end, end), code) + }) + } + } + + private async example(file: string) { + const uri = Uri.parse(file) + if (uri.scheme === 'http' || uri.scheme === 'https') { + const data = await this.httpGet(uri) + void this.tryIt('-- example \n' + data) + } else { + const doc = await workspace.openTextDocument(Uri.parse(file)) + void languages.setTextDocumentLanguage(doc, 'lean4') + await window.showTextDocument(doc, ViewColumn.One) + } + } + + private async receiveMessage(message: any) { + if (message.name === 'tryit') { + const code = message.contents as string + if (code) { + // hooray, we have some code to try! + // this initial comment makes the untitled editor tab have a more reasonable caption. + void this.tryIt('-- try it \n' + code) + } + } + } + + private webview?: WebviewPanel + private getWebview(): WebviewPanel { + if (!this.webview) { + const options: WebviewOptions & WebviewPanelOptions = { + enableFindWidget: true, + enableScripts: true, + enableCommandUris: true, + retainContextWhenHidden: true, + } + + this.webview = window.createWebviewPanel( + 'lean4_docview', + 'Lean Documentation', + { viewColumn: 3, preserveFocus: true }, + options, + ) + this.webview.onDidDispose(() => (this.webview = undefined)) + this.webview.webview.onDidReceiveMessage(m => this.receiveMessage(m)) + + let first = true + this.webview.onDidChangeViewState(async () => { + if (first) { + first = false + // super hacky way to show both infoview and docview in a split + await commands.executeCommand('workbench.action.focusRightGroup') + await commands.executeCommand('workbench.action.moveEditorToBelowGroup') + } + }) + } + return this.webview + } + + private async showAbbreviations(): Promise { + // display the HTML table definition of all abbreviations + if (this.abbreviations) { + const ac = new AbbreviationConfig() + const leader = ac.abbreviationCharacter.get() + const $ = cheerio.load( + '
AbbreviationUnicode Symbol
', + ) + const table = $('table') + for (const [abbr, sym] of Object.entries(this.abbreviations)) { + if (sym && sym.indexOf('CURSOR') < 0) { + const row = table.append($('')) + row.append($('').text(leader + abbr)) + row.append($('').text(sym)) + } + } + const help = $.html() + const uri = createLocalFileUrl(this.getTempFolder().createFile('help.html', help)) + return this.open(uri) + } + } + + private async httpGet(uri: Uri): Promise { + return new Promise(resolve => { + void axios.get(uri.toString(), { responseType: 'arraybuffer' }).then(response => { + if (response.status === 200) { + resolve(response.data as string) + } else { + resolve(`Error fetching ${uri.toString()}, code ${response.status}`) + } + }) + }) + } + + async fetch(url?: string): Promise { + if (url) { + try { + const uri = Uri.parse(url) + let fileType = '' + if (uri.scheme === 'file') { + fileType = extname(uri.fsPath) + if (fileType === '.html' || fileType === '.htm') { + return (await workspace.fs.readFile(uri)).toString() + } + } else { + const { data, headers } = await axios.get(url) + fileType = '' + headers['content-type'] + if (fileType.startsWith('text/html')) { + return data + } + } + + const $ = cheerio.load('

') + $('p') + .text(`Unsupported file type '${fileType}', please `) + .append($('').attr('href', url).attr('alwaysExternal', 'true').text('open in browser instead.')) + return $.html() + } catch (ex) { + const $ = cheerio.load('

') + $('p').text('Error fetching file. ' + ex) + return $.html() + } + } else { + const $ = cheerio.load('') + const body = $('body') + + const books: any = { + 'Theorem Proving in Lean': mkCommandUri( + 'lean4.docView.openUrl', + 'https://lean-lang.org/theorem_proving_in_lean4/introduction.html', + ), + 'Functional Programming in Lean': mkCommandUri( + 'lean4.docView.openUrl', + 'https://lean-lang.org/functional_programming_in_lean/', + ), + 'Mathematics in Lean': mkCommandUri( + 'lean4.docView.openUrl', + 'https://leanprover-community.github.io/mathematics_in_lean/', + ), + 'The Mechanics of Proof': mkCommandUri( + 'lean4.docView.openUrl', + 'https://hrmacbeth.github.io/math2001/', + ), + 'Reference Manual': mkCommandUri('lean4.docView.openUrl', 'https://lean-lang.org/lean4/doc/'), + 'Abbreviations Cheatsheet': mkCommandUri('lean4.docView.showAllAbbreviations'), + Example: mkCommandUri( + 'lean4.docView.openExample', + 'https://github.com/leanprover/lean4-samples/raw/main/HelloWorld/Main.lean', + ), + + // These are handy for testing that the bad file logic is working. + //'Test bad file': mkCommandUri('lean4.docView.openUrl', Uri.joinPath(this.extensionUri, 'media', 'webview.js')), + //'Test bad Uri': mkCommandUri('lean4.docView.openUrl', 'https://leanprover.github.io/lean4/doc/images/code-success.png'), + } + + for (const book of Object.getOwnPropertyNames(books)) { + body.append( + $('

').append( + $('') + .attr('href', books[book] as string) + .text(book), + ), + ) + } + + this.currentURL = createLocalFileUrl(this.getTempFolder().createFile('index.html', $.html())) + + return $.html() + } + } + + private mkRelativeUrl(relative: string, base: string): string { + const uri = new URL(relative, base) + if (uri.protocol === 'file:') { + if (new URL(base).protocol !== 'file:') { + return '' + } + const path = Uri.parse(uri.toString()).fsPath + if (this.webview) { + return this.webview.webview.asWebviewUri(Uri.parse(uri.toString())).toString() + } + return '' + } else { + return uri.toString() + } + } + + async getHtmlContents(): Promise { + return this.html ?? '' + } + + async setHtml(html?: string): Promise { + const { webview } = this.getWebview() + + const url = this.currentURL + let $: cheerio.Root + if (html) { + // See https://cheerio.js.org/ for cheerio API. + $ = cheerio.load(html) + } else { + try { + $ = cheerio.load(await this.fetch(url)) + } catch (e) { + $ = cheerio.load('

')
+                $('pre').text('' + e)
+            }
+        }
+
+        const book = 'book.js'
+        const bookScript = $(`script[src='${book}']`)
+        if (bookScript.length) {
+            const themes_uri = Uri.joinPath(this.extensionUri, 'media', 'themes.js')
+            const config = ``
+            const script_url = this.webview?.webview.asWebviewUri(themes_uri)
+            const node = $(``).insertBefore(bookScript)
+            $(config).insertBefore(node)
+        }
+
+        if (url) {
+            for (const style of $('link[rel=stylesheet]').get()) {
+                style.attribs.href = this.mkRelativeUrl(style.attribs.href as string, url)
+            }
+
+            for (const script of $('script[src]').get()) {
+                script.attribs.src = this.mkRelativeUrl(script.attribs.src as string, url)
+            }
+        }
+
+        for (const link of $('a[href]').get()) {
+            const tryItMatch = link.attribs.href.match(/\/(?:live|lean-web-editor)\/.*#code=(.*)/)
+            if (link.attribs.href.startsWith('#')) {
+                // keep in page fragment links
+            } else if (link.attribs.alwaysexternal) {
+                // keep links with always external attribute
+                // note: cheerio .attr('alwaysExternal', 'true') results in a lower case 'alwaysexternal'
+                // here when the html is round tripped through the cheerio parser.
+            } else if (link.attribs.tryitfile) {
+                link.attribs.title = link.attribs.title || 'Open code block (in existing file)'
+                link.attribs.href = mkCommandUri(
+                    'lean4.docView.openExample',
+                    new URL(link.attribs.tryitfile as string, url).toString(),
+                )
+            } else if (tryItMatch) {
+                const code = decodeURIComponent(tryItMatch[1] as string)
+                link.attribs.title = link.attribs.title || 'Open code block in new editor'
+                link.attribs.href = mkCommandUri('lean4.docView.openTryIt', code)
+            } else if (!link.attribs.href.startsWith('command:')) {
+                const hrefUrl = new URL(link.attribs.href as string, url)
+                const isExternal = !url || new URL(url).origin !== hrefUrl.origin
+                if (!isExternal || hrefUrl.protocol === 'file:') {
+                    link.attribs.title = link.attribs.title || link.attribs.href
+                    link.attribs.href = mkCommandUri('lean4.docView.openUrl', hrefUrl.toString())
+                }
+            }
+        }
+
+        // javascript search doesn't work
+        $('.sphinxsidebar #searchbox').remove()
+
+        const nav = $('