From 3293311a02af937be84d5a7c6b36a84e72555cf7 Mon Sep 17 00:00:00 2001
From: Timothee Lacroix <tlacroix@fb.com>
Date: Mon, 27 Sep 2021 15:59:52 +0200
Subject: [PATCH 1/2] export infoView API

---
 src/extension.ts |  7 +++++--
 src/infoview.ts  | 19 +++++++++++++++----
 2 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/src/extension.ts b/src/extension.ts
index e741075..9fbf744 100644
--- a/src/extension.ts
+++ b/src/extension.ts
@@ -43,7 +43,7 @@ const LEAN_MODE: DocumentFilter = {
     // scheme: 'file',
 };
 
-export async function activate(context: ExtensionContext): Promise<void> {
+export async function activate(context: ExtensionContext) {
     const isLean3 = await checkLean3();
     if (!isLean3) {
         return;
@@ -107,9 +107,10 @@ export async function activate(context: ExtensionContext): Promise<void> {
     context.subscriptions.push(new LeanStatusBarItem(server, roiManager));
 
     let staticServer = null;
+    let infoView : InfoProvider = null;
     function waitStaticServer() {
         // Add info view: listing either the current goal state or a list of all error messages
-        const infoView = new InfoProvider(server, LEAN_MODE, context, staticServer);
+        infoView = new InfoProvider(server, LEAN_MODE, context, staticServer);
         context.subscriptions.push(infoView);
         context.subscriptions.push(new DocViewProvider(staticServer));
         // Tactic suggestions
@@ -128,4 +129,6 @@ export async function activate(context: ExtensionContext): Promise<void> {
 
     context.subscriptions.push(languages.registerDocumentLinkProvider(LEAN_MODE,
         new LibraryNoteLinkProvider()));
+
+    return {'infoView': infoView}; // export infoView for other plugins to use
 }
diff --git a/src/infoview.ts b/src/infoview.ts
index 851f75b..ab53a4f 100644
--- a/src/infoview.ts
+++ b/src/infoview.ts
@@ -28,8 +28,10 @@ export class InfoProvider implements Disposable {
 
     private hoverDecorationType: TextEditorDecorationType;
 
-    constructor(private server: Server, private leanDocs: DocumentSelector, private context: ExtensionContext, private staticServer?: StaticServer) {
+    // Callbacks when a new tactic state is received
+    private tacticStateHandlers: { [id: string] : (string) => void; } = {};
 
+    constructor(private server: Server, private leanDocs: DocumentSelector, private context: ExtensionContext, private staticServer?: StaticServer) {
         this.statusBarItem = window.createStatusBarItem(StatusBarAlignment.Right, 1000);
 
         this.hoverDecorationType = window.createTextEditorDecorationType({
@@ -108,6 +110,10 @@ export class InfoProvider implements Disposable {
         }
     }
 
+    onNewTacticState(handler_name: string, handler: (string) => void) {
+        this.tacticStateHandlers[handler_name] = handler;
+    }
+
     private makeProxyConnection() {
         if (this.proxyConnection) {
             this.proxyConnection.dispose();
@@ -120,12 +126,17 @@ export class InfoProvider implements Disposable {
                     payload: JSON.stringify(e)
                 })
             ),
-            this.proxyConnection.jsonMessage.on(e =>
+            this.proxyConnection.jsonMessage.on(e => {
+                if ('record' in e && 'state' in e.record){
+                    for (const [handlerName, handler] of Object.entries(this.tacticStateHandlers)) {
+                        handler(e.record.state);
+                    }
+                }
                 this.postMessage({
                     command: 'server_event',
                     payload: JSON.stringify(e)
-                })
-            )
+                });
+            })
         );
 
     }

From 1290949f00695a433334cd2d49c756ca4257cede Mon Sep 17 00:00:00 2001
From: Xavier Martinet <xavierm@fb.com>
Date: Tue, 12 Oct 2021 16:11:01 +0200
Subject: [PATCH 2/2] pass widget as callback arg

---
 src/infoview.ts | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/infoview.ts b/src/infoview.ts
index ab53a4f..dcf2ede 100644
--- a/src/infoview.ts
+++ b/src/infoview.ts
@@ -29,7 +29,7 @@ export class InfoProvider implements Disposable {
     private hoverDecorationType: TextEditorDecorationType;
 
     // Callbacks when a new tactic state is received
-    private tacticStateHandlers: { [id: string] : (string) => void; } = {};
+    private tacticStateHandlers: { [id: string] : (state: string, widget: object) => void; } = {};
 
     constructor(private server: Server, private leanDocs: DocumentSelector, private context: ExtensionContext, private staticServer?: StaticServer) {
         this.statusBarItem = window.createStatusBarItem(StatusBarAlignment.Right, 1000);
@@ -110,7 +110,7 @@ export class InfoProvider implements Disposable {
         }
     }
 
-    onNewTacticState(handler_name: string, handler: (string) => void) {
+    onNewTacticState(handler_name: string, handler: (state: string, widget: object) => void): void {
         this.tacticStateHandlers[handler_name] = handler;
     }
 
@@ -127,9 +127,9 @@ export class InfoProvider implements Disposable {
                 })
             ),
             this.proxyConnection.jsonMessage.on(e => {
-                if ('record' in e && 'state' in e.record){
+                if ('record' in e && 'state' in e.record && 'widget' in e.record){
                     for (const [handlerName, handler] of Object.entries(this.tacticStateHandlers)) {
-                        handler(e.record.state);
+                        handler(e.record.state, e.record.widget);
                     }
                 }
                 this.postMessage({