Get position

[javier-m]

Added the widget argument (containing line and column) to the callback

[gebner]

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;

[gebner]

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.

[gebner]

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':