From d5bdf6c49e554b484eede0ecdc8cb92fe848722c Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 14 May 2020 15:43:22 +0200
Subject: [PATCH] Add library note link provider.

---
 src/extension.ts   |  4 ++++
 src/librarynote.ts | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 src/librarynote.ts

diff --git a/src/extension.ts b/src/extension.ts
index e8de7e3..be22a4c 100644
--- a/src/extension.ts
+++ b/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()));
 }
diff --git a/src/librarynote.ts b/src/librarynote.ts
new file mode 100644
index 0000000..9d414d2
--- /dev/null
+++ b/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.`);
+    }
+}
\ No newline at end of file