Add library note link provider.

src/extension.ts

@@ -18,6 +18,7 @@ import { LeanStatusBarItem } from './statusbar';
 import { LeanSyncService } from './sync';
 import { LeanTaskGutter, LeanTaskMessages } from './taskgutter';
 import { StaticServer } from './staticserver';
+import { LibraryNoteLinkProvider } from './librarynote';
 
 // Seeing .olean files in the source tree is annoying, we should
 // just globally hide them.
@@ -124,4 +125,7 @@ export function activate(context: ExtensionContext) {
     });
 
     context.subscriptions.push(new LeanpkgService(server));
+
+    context.subscriptions.push(languages.registerDocumentLinkProvider(LEAN_MODE,
+        new LibraryNoteLinkProvider()));
 }

src/librarynote.ts

@@ -0,0 +1,33 @@
+import {DocumentLinkProvider, TextDocument, DocumentLink, ProviderResult, Range, workspace, window} from 'vscode';
+
+const seeNoteRegex = /see note \[([^\]]+)\]/gi;
+const libraryNoteRegex = /library_note "(.*)"/g;
+
+export class LibraryNoteLinkProvider implements DocumentLinkProvider {
+    provideDocumentLinks(document: TextDocument): ProviderResult<DocumentLink[]> {
+        const links: DocumentLink[] = [];
+        for (const m of document.getText().matchAll(seeNoteRegex)) {
+            const link = new DocumentLink(new Range(
+                document.positionAt(m.index), document.positionAt(m.index + m[0].length)));
+            link.tooltip = m[1];
+            links.push(link);
+        }
+        return links;
+    }
+
+    async resolveDocumentLink(link: DocumentLink): Promise<DocumentLink> {
+        const noteName = link.tooltip;
+        for (const leanFile of await workspace.findFiles('**/*.lean')) {
+            const content = (await workspace.fs.readFile(leanFile)).toString();
+            for (const m of content.matchAll(libraryNoteRegex)) {
+                console.log(m[1]);
+                if (m[1] === noteName) {
+                    const lineNo = content.substr(0, m.index).split(/\r\n|\r|\n/).length;
+                    link.target = leanFile.with({ fragment: `L${lineNo}` });
+                    return link;
+                }
+            }
+        }
+        window.showErrorMessage(`Library note "${noteName}" not found.`);
+    }
+}