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 { +export async function activate(context: ExtensionContext) { const isLean3 = await checkLean3(); if (!isLean3) { return; @@ -107,9 +107,10 @@ export async function activate(context: ExtensionContext): Promise { 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 { 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..dcf2ede 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] : (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); this.hoverDecorationType = window.createTextEditorDecorationType({ @@ -108,6 +110,10 @@ export class InfoProvider implements Disposable { } } + onNewTacticState(handler_name: string, handler: (state: string, widget: object) => void): 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 && 'widget' in e.record){ + for (const [handlerName, handler] of Object.entries(this.tacticStateHandlers)) { + handler(e.record.state, e.record.widget); + } + } this.postMessage({ command: 'server_event', payload: JSON.stringify(e) - }) - ) + }); + }) ); }