Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Get position #281

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Get position #281

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3293311
export infoView API
Sep 27, 2021
1290949
pass widget as callback arg
javier-m Oct 12, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions src/extension.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
return {'infoView': infoView}; // export infoView for other plugins to use
return {onNewTacticState: infoView.onNewTacticState}; // export infoView for other plugins to use

I'd rather export only the event.

}
19 changes: 15 additions & 4 deletions src/infoview.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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({
Expand Down Expand Up @@ -108,6 +110,10 @@ export class InfoProvider implements Disposable {
}
}

onNewTacticState(handler_name: string, handler: (state: string, widget: object) => void): void {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
onNewTacticState(handler_name: string, handler: (state: string, widget: object) => void): void {
onNewTacticState(handler_name: string, handler: (loc: Location, state: InfoResponse) => void): void {

The widget field doesn't really contain any information (it's an id that you pass to the get_widget command). You probably also want the location (filename & position) so that you can insert something there.

Can you explain what the handler_name should be? Is this the name of the other extension?

I'm not sure if it's possible, but the nicest way would be to use the EventEmitter class from vscode:

    private onNewTacticStateEmitter = new EventEmitter<{ location: Location, info: InfoResponse }>();
    onNewTacticState = this.onNewTacticStateEmitter.event;

this.tacticStateHandlers[handler_name] = handler;
}

private makeProxyConnection() {
if (this.proxyConnection) {
this.proxyConnection.dispose();
Expand All @@ -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){
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This will trigger on every hover as well (i.e., when you move the mouse around). A better place to intercept would be here:

vscode-lean/infoview/info.tsx

Line 173 in 2b43982


You'd then need to send a message from the webview back to the extension like this:

vscode-lean/infoview/server.ts

Lines 25 to 27 in 2b43982

export function copyText(text: string): void {
post({ command: 'copy_text', text});
}

And receive the message here:

vscode-lean/src/infoview.ts

Line 195 in 2b43982

case 'copy_text':

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)
})
)
});
})
);

}
Expand Down