fix: translate between utf16 code unit offsets (vscode) and codepoints (lean)

src/completion.ts

@@ -2,6 +2,7 @@ import { CompletionItem, CompletionItemKind, CompletionItemProvider,
     MarkdownString, Position, Range, TextDocument, workspace } from 'vscode';
 import { Server } from './server';
 import { isInputCompletion } from './util';
+import { CodePointPosition } from './utils/utf16Position';
 
 const keywords = [
     'theorem', 'lemma', 'axiom', 'axioms', 'variable', 'protected', 'private',
@@ -42,7 +43,8 @@ export class LeanCompletionItemProvider implements CompletionItemProvider {
             Promise<CompletionItem[]> {
         // TODO(gabriel): use LeanInputAbbreviator.active() instead
         if (!isInputCompletion(document, position)) {
-            const message = await this.server.complete(document.fileName, position.line + 1, position.character);
+            const codePointPosition = CodePointPosition.ofPosition(document, position);
+            const message = await this.server.complete(document.fileName, codePointPosition.line + 1, codePointPosition.character);
             const completions: CompletionItem[] = [];
             if (message.completions) {
                 for (const completion of message.completions) {

src/definition.ts

@@ -1,5 +1,6 @@
 import { Definition, DefinitionProvider, Location, Position, TextDocument, Uri } from 'vscode';
 import { Server } from './server';
+import { CodePointPosition } from './utils/utf16Position';
 
 export class LeanDefinitionProvider implements DefinitionProvider {
     server: Server;
@@ -9,11 +10,13 @@ export class LeanDefinitionProvider implements DefinitionProvider {
     }
 
     async provideDefinition(document: TextDocument, position: Position): Promise<Definition> {
-        const response = await this.server.info(document.fileName, position.line + 1, position.character);
+        const codePointPosition = CodePointPosition.ofPosition(document, position);
+        const response = await this.server.info(document.fileName, codePointPosition.line + 1, codePointPosition.character);
         if (response.record && response.record.source) {
             const src = response.record.source;
             const uri = src.file ? Uri.file(src.file) : document.uri;
-            return new Location(uri, new Position(src.line - 1, src.column));
+            const pos = new CodePointPosition(src.line - 1, src.column);
+            return new Location(uri, pos.toPosition(document));
         } else {
             return null;
         }

src/diagnostics.ts

@@ -2,6 +2,7 @@ import { Message, Severity } from 'lean-client-js-node';
 import { Diagnostic, DiagnosticCollection, DiagnosticSeverity,
     Disposable, languages, Position, Range, TextDocument, Uri, workspace } from 'vscode';
 import { Server } from './server';
+import { CodePointPosition } from './utils/utf16Position';
 
 function toSeverity(severity: Severity): DiagnosticSeverity {
     switch (severity) {
@@ -56,16 +57,22 @@ export class LeanDiagnosticsProvider implements Disposable {
         messages = truncateMessages(messages);
 
         for (const message of messages) {
-            const line = Math.max(message.pos_line - 1, 0);
-            const pos = new Position(line, message.pos_col);
             // Assign the diagnostic to the entire word following the info message
             // so that code actions can be activated more easily
             let msgDoc = docMap.get(message.file_name);
             if (!msgDoc) {
                 msgDoc = workspace.textDocuments.find((doc) => doc.fileName === message.file_name);
                 docMap.set(message.file_name, msgDoc);
             }
-            const range = msgDoc.getWordRangeAtPosition(pos) || new Range(pos, pos);
+            const pos = new CodePointPosition(Math.max(message.pos_line - 1, 0), message.pos_col);
+            const endPos = message.end_pos_col !== undefined
+                ? new CodePointPosition(Math.max(message.end_pos_line - 1, 0), message.end_pos_col)
+                : undefined;
+            const utf16Pos = pos.toPosition(msgDoc);
+            const utf16EndPos = endPos?.toPosition(msgDoc);
+            const range = endPos
+                ? new Range(utf16Pos, utf16EndPos)
+                : msgDoc.getWordRangeAtPosition(utf16Pos) || new Range(utf16Pos, utf16Pos);
             let diagnostics = diagnosticMap.get(message.file_name);
             if (!diagnostics) { diagnosticMap.set(message.file_name, diagnostics = []); }
             const d = new Diagnostic(range, message.text,

src/holes.ts

@@ -1,17 +1,20 @@
 import { HoleCommands, HoleResponse } from 'lean-client-js-core';
 import { CodeActionProvider, Command, commands, Diagnostic,
     DiagnosticCollection, DiagnosticSeverity, Disposable, DocumentSelector, languages,
-    Range, TextDocument, Uri, window } from 'vscode';
+    Range, TextDocument, TextEditor, Uri, window } from 'vscode';
 import { Server } from './server';
+import { CodePointPosition } from './utils/utf16Position';
 
 interface Pos { line: number; column: number }
 interface Ran { start: Pos; end: Pos }
-function mkRange(r: Ran): Range {
-    return new Range(r.start.line - 1, r.start.column, r.end.line - 1, r.end.column);
+function mkRange(doc: TextDocument, r: Ran): Range {
+    const startPos = new CodePointPosition(r.start.line - 1, r.start.column);
+    const endPos = new CodePointPosition(r.end.line - 1, r.end.column);
+    return new Range(startPos.toPosition(doc), endPos.toPosition(doc));
 }
 
 export class LeanHoles implements Disposable, CodeActionProvider {
-    private holes: HoleCommands[] = [];
+    private holes: [TextDocument, HoleCommands][] = [];
     private collection: DiagnosticCollection;
     private subscriptions: Disposable[] = [];
 
@@ -31,26 +34,30 @@ export class LeanHoles implements Disposable, CodeActionProvider {
     private async refresh() {
         if (!this.server.alive()) { return; }
         try {
-            const ress = await Promise.all(window.visibleTextEditors
-                .filter((editor) => languages.match(this.leanDocs, editor.document))
-                .map((editor) => this.server.allHoleCommands(editor.document.fileName)));
+            const leanEditor = window.visibleTextEditors .filter((editor) =>
+                languages.match(this.leanDocs, editor.document));
+            const ress = await Promise.all(leanEditor
+                .map((editor) =>  this.server.allHoleCommands(editor.document.fileName).then
+                    ((holes) : [TextDocument, any] => [editor.document, holes])));
 
             this.holes = [];
-            for (const res of ress) {
-                [].push.apply(this.holes, res.holes);
+            for (const [document, res] of ress) {
+                for (const hole of res.holes) {
+                    this.holes.push([document, hole]);
+                }
             }
 
-            const holesPerFile = new Map<string, HoleCommands[]>();
-            for (const hole of this.holes) {
+            const holesPerFile = new Map<string, [TextDocument, HoleCommands][]>();
+            for (const [document, hole] of this.holes) {
                 if (!holesPerFile.get(hole.file)) { holesPerFile.set(hole.file, []); }
-                holesPerFile.get(hole.file).push(hole);
+                holesPerFile.get(hole.file).push([document, hole]);
             }
 
             this.collection.clear();
             for (const file of holesPerFile.keys()) {
                 this.collection.set(Uri.file(file),
-                    holesPerFile.get(file).map((hole) =>
-                        new Diagnostic(mkRange(hole),
+                    holesPerFile.get(file).map(([editor, hole]) =>
+                        new Diagnostic(mkRange(editor, hole),
                             'Hole: ' + hole.results.map((a) => a.name).join('/'),
                             DiagnosticSeverity.Hint)));
             }
@@ -75,7 +82,7 @@ export class LeanHoles implements Disposable, CodeActionProvider {
             for (const editor of window.visibleTextEditors) {
                 if (editor.document.fileName === file) {
                     await editor.edit((builder) => {
-                        builder.replace(mkRange(res.replacements),
+                        builder.replace(mkRange(editor.document, res.replacements),
                             res.replacements.alternatives[0].code);
                     });
                 }
@@ -85,8 +92,8 @@ export class LeanHoles implements Disposable, CodeActionProvider {
 
     provideCodeActions(document: TextDocument, range: Range): Command[] {
         const cmds: Command[] = [];
-        for (const hole of this.holes) {
-            if (!range.intersection(mkRange(hole))) { continue; }
+        for (const [document, hole] of this.holes) {
+            if (!range.intersection(mkRange(document, hole))) { continue; }
             for (const action of hole.results) {
                 cmds.push({
                     title: action.description,

src/hover.ts

@@ -1,5 +1,6 @@
 import { Hover, HoverProvider, MarkdownString, Position, Range, TextDocument } from 'vscode';
 import { Server } from './server';
+import { CodePointPosition } from './utils/utf16Position';
 
 export class LeanHoverProvider implements HoverProvider {
     server: Server;
@@ -9,7 +10,8 @@ export class LeanHoverProvider implements HoverProvider {
     }
 
     async provideHover(document: TextDocument, position: Position): Promise<Hover> {
-        const response = await this.server.info(document.fileName, position.line + 1, position.character);
+        const codePointPosition = CodePointPosition.ofPosition(document, position);
+        const response = await this.server.info(document.fileName, codePointPosition.line + 1, codePointPosition.character);
         if (response.record) {
             const contents: MarkdownString[] = [];
             const name = response.record['full-id'] || response.record.text;
@@ -30,8 +32,7 @@ export class LeanHoverProvider implements HoverProvider {
                 contents.push(new MarkdownString()
                     .appendCodeblock(response.record.state, 'lean'));
             }
-            const pos = new Position(position.line - 1, position.character);
-            return new Hover(contents, new Range(pos, pos));
+            return new Hover(contents, new Range(position, position));
         }
     }
 }

src/infoview.ts

@@ -10,6 +10,7 @@ import {
 import { Server } from './server';
 import { ToInfoviewMessage, FromInfoviewMessage, PinnedLocation, InsertTextMessage, ServerRequestMessage, RevealMessage, HoverPositionMessage, locationEq, Location, InfoViewTacticStateFilter } from './shared'
 import { StaticServer } from './staticserver';
+import { CodePointPosition } from './utils/utf16Position';
 
 export class InfoProvider implements Disposable {
     /** Instance of the panel. */
@@ -60,7 +61,7 @@ export class InfoProvider implements Disposable {
                     let changed: boolean = false;
                     this.pins = this.pins.map(pin => {
                         if (pin.file_name !== e.document.fileName) { return pin; }
-                        let newPosition = this.positionOfLocation(pin);
+                        let newPosition = this.positionOfLocation(pin).toPosition(e.document);
                         for (const chg of e.contentChanges) {
                             if (newPosition.isAfterOrEqual(chg.range.start)) {
                                 let lines = 0;
@@ -76,7 +77,7 @@ export class InfoProvider implements Disposable {
                             }
                         }
                         newPosition = e.document.validatePosition(newPosition);
-                        const new_pin = this.makeLocation(pin.file_name, newPosition);
+                        const new_pin = this.makeLocation(pin.file_name, CodePointPosition.ofPosition(e.document, newPosition));
                         if (!locationEq(new_pin, pin)) {changed = true; }
                         return { ...new_pin, key: pin.key };
                     });
@@ -235,7 +236,7 @@ export class InfoProvider implements Disposable {
             }
         }
         if (!editor) {return; }
-        const pos = message.loc ? this.positionOfLocation(message.loc) : editor.selection.active;
+        const pos = message.loc ? this.positionOfLocation(message.loc).toPosition(editor.document) : editor.selection.active;
         const insert_type = message.insert_type ?? 'relative';
         if (insert_type === 'relative') {
             // in this case, assume that we actually want to insert at the same
@@ -261,10 +262,10 @@ export class InfoProvider implements Disposable {
         }
     }
 
-    private positionOfLocation(l: Location): Position {
-        return new Position(l.line - 1, l.column ?? 0);
+    private positionOfLocation(l: Location): CodePointPosition {
+        return new CodePointPosition(l.line - 1, l.column ?? 0);
     }
-    private makeLocation(file_name: string, pos: Position): Location {
+    private makeLocation(file_name: string, pos: CodePointPosition): Location {
         return {
             file_name,
             line: pos.line + 1,
@@ -293,7 +294,6 @@ export class InfoProvider implements Disposable {
     }
 
     private async revealEditorPosition(uri: Uri, line: number, column: number) {
-        const pos = new Position(line - 1, column);
         let editor = null;
         for (const e of window.visibleTextEditors) {
             if (e.document.uri.toString() === uri.toString()) {
@@ -306,6 +306,7 @@ export class InfoProvider implements Disposable {
             const td = await workspace.openTextDocument(uri);
             editor = await window.showTextDocument(td, c, false);
         }
+        const pos = new CodePointPosition(line - 1, column).toPosition(editor.document);
         editor.revealRange(new Range(pos, pos), TextEditorRevealType.InCenterIfOutsideViewport);
         editor.selection = new Selection(pos, pos);
         return;
@@ -317,9 +318,9 @@ export class InfoProvider implements Disposable {
         const endColumn = column;
         for (const editor of window.visibleTextEditors) {
             if (editor.document.uri.path === file_name) {
-                const pos = new Position(line - 1, column);
-                const endPos = new Position(endLine - 1, endColumn);
-                const range = new Range(pos, endPos);
+                const pos = new CodePointPosition(line - 1, column);
+                const endPos = new CodePointPosition(endLine - 1, endColumn);
+                const range = new Range(pos.toPosition(editor.document), endPos.toPosition(editor.document));
                 editor.setDecorations(this.hoverDecorationType, [range]);
             }
         }
@@ -344,7 +345,8 @@ export class InfoProvider implements Disposable {
 
     private getActiveCursorLocation(): Location | null {
         if (!window.activeTextEditor || !languages.match(this.leanDocs, window.activeTextEditor.document)) {return null; }
-        return this.makeLocation(window.activeTextEditor.document.fileName, window.activeTextEditor.selection.active);
+        let p = CodePointPosition.ofPosition(window.activeTextEditor.document, window.activeTextEditor.selection.active);
+        return this.makeLocation(window.activeTextEditor.document.fileName, p);
     }
 
     private updateTypeStatus(info: InfoResponse) {

src/search.ts

@@ -1,18 +1,20 @@
-import { Location, Position, SymbolInformation, SymbolKind, Uri, WorkspaceSymbolProvider } from 'vscode';
+import { CancellationToken, Location, Position, ProviderResult, SymbolInformation, SymbolKind, Uri, workspace, WorkspaceSymbolProvider } from 'vscode';
 import { Server } from './server';
+import { CodePointPosition } from './utils/utf16Position';
 
 export class LeanWorkspaceSymbolProvider implements WorkspaceSymbolProvider {
     constructor(private server: Server) {}
 
     async provideWorkspaceSymbols(query: string): Promise<SymbolInformation[]> {
         const response = await this.server.search(query);
-        return response.results
+        return await Promise.all(response.results
             .filter((item) => item.source && item.source.file &&
                 item.source.line && item.source.column)
-            .map((item) => {
+            .map(async (item) => {
+                const document = await workspace.openTextDocument(Uri.file(item.source.file));
                 const loc = new Location(Uri.file(item.source.file),
-                    new Position(item.source.line - 1, item.source.column));
+                    new CodePointPosition(item.source.line - 1, item.source.column).toPosition(document));
                 return new SymbolInformation(item.text, SymbolKind.Function, item.type, loc);
-            });
+            }));
     }
 }

src/tacticsuggestions.ts

@@ -5,6 +5,7 @@ import { CodeActionContext, CodeActionProvider, Command, commands,
 import { InfoProvider } from './infoview';
 import { Server } from './server';
 import { regexGM, magicWord, regexM } from './trythis';
+import { CodePointPosition } from './utils/utf16Position';
 
 /** Pastes suggestions provided by tactics such as `squeeze_simp` */
 export class TacticSuggestions implements Disposable, CodeActionProvider {
@@ -49,7 +50,7 @@ export class TacticSuggestions implements Disposable, CodeActionProvider {
 
     private findSelectedMessage(textEditor: TextEditor) {
         const curFileName = textEditor.document.fileName;
-        const curPosition = textEditor.selection.active;
+        const curPosition = CodePointPosition.ofPosition(textEditor.document, textEditor.selection.active);
         // Find message closest to the cursor
         const messages = this.server.messages
             .filter((m: Message) => m.file_name === curFileName &&
@@ -73,8 +74,9 @@ export class TacticSuggestions implements Disposable, CodeActionProvider {
         suggestion = suggestion.trim();
 
         // Start of the tactic call to replace
-        const startLine = m.pos_line - 1;
-        let startCol = m.pos_col;
+        const startPos = new CodePointPosition(m.pos_line - 1, m.pos_col).toPosition(textEditor.document);
+        const startLine = startPos.line;
+        let startCol = startPos.character;
 
         // Try to determine the end of the tactic call to replace.
         // Heuristic: Find the next comma, semicolon, unmatched closing bracket,