Rewrite of the abbreviation feature.

.eslintrc.js

@@ -116,7 +116,7 @@ module.exports = {
         "no-throw-literal": "error",
         "no-trailing-spaces": "error",
         "no-undef-init": "error",
-        "no-underscore-dangle": "error",
+        "no-underscore-dangle": "off",
         "no-unsafe-finally": "error",
         "no-unused-expressions": "error",
         "no-unused-labels": "error",

README.md

@@ -125,6 +125,8 @@ This extension contributes the following settings (for a complete list, open the
 
 ### Input / editing settings
 
+* `lean.input.eagerReplacementEnabled`: enables/disables eager replacement as soon as the abbreviation is unique (`true` by default)
+
 * `lean.input.leader`: character to type to trigger Unicode input mode (`\` by default)
 
 * `lean.input.languages`: allows the Unicode input functionality to be used in other languages

package.json

@@ -88,6 +88,11 @@
 					"default": "\\",
 					"markdownDescription": "Leader key to trigger input mode."
 				},
+				"lean.input.eagerReplacementEnabled": {
+					"type": "boolean",
+					"default": true,
+					"markdownDescription": "Enable eager replacement of abbreviations that uniquely identify a symbol."
+				},
 				"lean.infoViewAllErrorsOnLine": {
 					"type": "boolean",
 					"default": false,
@@ -341,12 +346,6 @@
 				"mac": "tab",
 				"when": "editorTextFocus && editorLangId == lean && lean.input.isActive"
 			},
-			{
-				"command": "lean.input.convertWithNewline",
-				"key": "enter",
-				"mac": "enter",
-				"when": "editorTextFocus && editorLangId == lean && lean.input.isActive && !suggestWidgetVisible && !renameInputVisible && !inSnippetMode && !quickFixWidgetVisible && !vim.active || editorTextFocus && editorLangId == lean && lean.input.isActive && !suggestWidgetVisible && !renameInputVisible && !inSnippetMode && !quickFixWidgetVisible && vim.mode == 'Insert'"
-			},
 			{
 				"command": "lean.batchExecute",
 				"key": "ctrl+shift+r",
@@ -431,6 +430,7 @@
 		"lean-client-js-core": "^1.5.0",
 		"lean-client-js-node": "^1.5.0",
 		"load-json-file": "6.2.0",
+		"mobx": "5.15.7",
 		"react-katex": "^2.0.2",
 		"semver": "^7.3.2",
 		"username": "^5.1.0"

src/abbreviation/AbbreviationHoverProvider.ts

@@ -0,0 +1,48 @@
+import { HoverProvider, TextDocument, Position, Hover, Range } 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 abbrevations: AbbreviationProvider
+	) {}
+
+	provideHover(document: TextDocument, pos: Position): Hover | undefined {
+		const context = document.lineAt(pos.line).text.substr(pos.character);
+		const symbolsAtCursor = this.abbrevations.findSymbolsIn(context);
+		const allAbbrevs = symbolsAtCursor.map((symbol) => ({
+			symbol,
+			abbrevs: this.abbrevations.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 }) =>
+					`Type ${symbol} using ${abbrevs
+						.map((a) => '`' + leader + a + '`')
+						.join(' or ')}`
+			)
+			.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);
+	}
+}

src/abbreviation/AbbreviationProvider.ts

@@ -0,0 +1,95 @@
+import { computed } from 'mobx';
+import { Disposable } from 'vscode';
+import { autorunDisposable } from '../utils/autorunDisposable';
+import * as abbreviations from './abbreviations.json';
+import { SymbolsByAbbreviation, AbbreviationConfig } 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> = {};
+
+	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 = {};
+			})
+		);
+	}
+
+	@computed
+	private 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);
+	}
+
+	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()];
+	}
+
+	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 {
+		const matchingSymbol = this.findSymbolsByAbbreviationPrefix(abbrev)[0];
+		if (matchingSymbol) {
+			return matchingSymbol;
+		} else if (abbrev.length > 0) {
+			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();
+		}
+	}
+}

src/abbreviation/README.md

@@ -0,0 +1,33 @@
+# 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.
+
+### 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)

translations.json → src/abbreviation/abbreviations.json

@@ -1,4 +1,18 @@
 {
+    "{}": "{$CURSOR}",
+    "{}_": "{$CURSOR}_",
+    "{{}}": "⦃$CURSOR⦄",
+    "[]": "[$CURSOR]",
+    "[]_": "[$CURSOR]_",
+    "[[]]": "⟦$CURSOR⟧",
+    "<>": "⟨$CURSOR⟩",
+    "()": "($CURSOR)",
+    "()_": "($CURSOR)_",
+    "([])'": "⟮$CURSOR⟯",
+    "f<>": "‹$CURSOR›",
+    "f<<>>": "«$CURSOR»",
+    "[--]": "⁅$CURSOR⁆",
+    "\\": "\\",
     "a": "α",
     "b": "β",
     "c": "χ",
@@ -1347,7 +1361,7 @@
     "bfX": "𝐗",
     "bfY": "𝐘",
     "bfZ": "𝐙",
-    
+
     "bfa": "𝐚",
     "bfb": "𝐛",
     "bfc": "𝐜",
@@ -1739,5 +1753,4 @@
     "Vdash": "⊩",
     "Vert": "‖",
     "Vvdash": "⊪"
-
 }

src/abbreviation/config.ts

@@ -0,0 +1,36 @@
+import { serializerWithDefault, VsCodeSetting } from '../utils/VsCodeSetting';
+
+/**
+ * Exposes (observable) settings for the abbreviation feature.
+ */
+export class AbbreviationConfig {
+	readonly inputModeEnabled = new VsCodeSetting('lean.input.enabled', {
+		serializer: serializerWithDefault(true),
+	});
+
+	readonly abbreviationCharacter = new VsCodeSetting('lean.input.leader', {
+		serializer: serializerWithDefault('\\'),
+	});
+
+	readonly languages = new VsCodeSetting('lean.input.languages', {
+		serializer: serializerWithDefault(['lean']),
+	});
+
+	readonly inputModeCustomTranslations = new VsCodeSetting(
+		'lean.input.customTranslations',
+		{
+			serializer: serializerWithDefault<SymbolsByAbbreviation>({}),
+		}
+	);
+
+	readonly eagerReplacementEnabled = new VsCodeSetting(
+		'lean.input.eagerReplacementEnabled',
+		{
+			serializer: serializerWithDefault(true),
+		}
+	);
+}
+
+export interface SymbolsByAbbreviation {
+	[abbrev: string]: string;
+}

src/abbreviation/index.ts

@@ -0,0 +1,33 @@
+import { Disposable, languages } from 'vscode';
+import { autorunDisposable } from '../utils/autorunDisposable';
+import { AbbreviationHoverProvider } from './AbbreviationHoverProvider';
+import { AbbreviationProvider } from './AbbreviationProvider';
+import { AbbreviationRewriterFeature } from './rewriter/AbbreviationRewriterFeature';
+import { AbbreviationConfig } from './config';
+
+export class AbbreviationFeature {
+	private readonly disposables = new Array<Disposable>();
+
+	constructor() {
+		const config = new AbbreviationConfig();
+		const abbrevations = new AbbreviationProvider(config);
+
+		this.disposables.push(
+			autorunDisposable((disposables) => {
+				disposables.push(
+					languages.registerHoverProvider(
+						config.languages.get(),
+						new AbbreviationHoverProvider(config, abbrevations)
+					)
+				);
+			}),
+			new AbbreviationRewriterFeature(config, abbrevations)
+		);
+	}
+
+	dispose(): void {
+		for (const d of this.disposables) {
+			d.dispose();
+		}
+	}
+}