Add widget effect support for specifying location of text to insert.

infoview/server.ts

@@ -1,5 +1,5 @@
 import { Server, Transport, Connection, Event, TransportError, Message } from 'lean-client-js-core';
-import { ToInfoviewMessage, FromInfoviewMessage, Config, Location, defaultConfig, PinnedLocation } from '../src/shared';
+import { ToInfoviewMessage, FromInfoviewMessage, Config, Location, defaultConfig, PinnedLocation, InsertTextMessage } from '../src/shared';
 declare const acquireVsCodeApi;
 const vscode = acquireVsCodeApi();
 
@@ -10,15 +10,15 @@ export function post(message: FromInfoviewMessage): void { // send a message to
 export function clearHighlight(): void { return post({ command: 'stop_hover'}); }
 export function highlightPosition(loc: Location): void { return post({ command: 'hover_position', loc}); }
 export function copyToComment(text: string): void {
-    post({ command: 'insert_text', text: `/-\n${text}\n-/\n`});
+    post({ command: 'insert_text', text: `/-\n${text}\n-/\n`, insert_type: 'relative'});
 }
 
 export function reveal(loc: Location): void {
     post({ command: 'reveal', loc });
 }
 
-export function edit(loc: Location, text: string): void {
-    post({ command: 'insert_text', loc, text });
+export function edit(loc: Location, text: string, insert_type : InsertTextMessage['insert_type'] = 'relative'): void {
+    post({ command: 'insert_text', loc, text, insert_type });
 }
 
 export function copyText(text: string): void {

infoview/widget.tsx

@@ -72,7 +72,7 @@ class WidgetErrorBoundary extends React.Component<{children: any},{error?: {mess
 
 /** [todo] pending adding to lean-client-js */
 export type WidgetEffect =
-| {kind: 'insert_text'; text: string}
+| {kind: 'insert_text', text: string, line?: number; column?: number; file_name?: string; insert_type?: 'relative' | 'absolute'}
 | {kind: 'reveal_position'; file_name: string; line: number; column: number}
 | {kind: 'highlight_position'; file_name: string; line: number; column: number}
 | {kind: 'clear_highlighting'}
@@ -82,8 +82,15 @@ export type WidgetEffect =
 function applyWidgetEffect(widget: WidgetIdentifier, file_name: string, effect: WidgetEffect) {
     switch (effect.kind) {
         case 'insert_text':
-            const loc = {file_name, line: widget.line, column: widget.column};
-            edit(loc, effect.text);
+            const insert_type = effect.insert_type ?? 'relative';
+            if (insert_type === 'relative') {
+                const line = widget.line + (effect.line ?? 0);
+                edit({file_name, line, column:0}, effect.text, 'relative');
+            } else if (insert_type === 'absolute') {
+                edit({file_name:effect.file_name ?? file_name, line: effect.line, column: effect.column}, effect.text, 'absolute')
+            } else {
+                throw new Error(`unrecognised effect insert type ${insert_type}`);
+            }
             break;
         case 'reveal_position': reveal({file_name: effect.file_name || file_name, line: effect.line, column: effect.column}); break;
         case 'highlight_position': highlightPosition({file_name: effect.file_name || file_name, line: effect.line, column: effect.column}); break;

src/infoview.ts

@@ -215,7 +215,6 @@ export class InfoProvider implements Disposable {
         this.proxyConnection.send(JSON.parse(message.payload));
     }
     private async handleInsertText(message: InsertTextMessage) {
-        const new_command = message.text;
         let editor: TextEditor = null;
         if (message.loc) {
            editor = window.visibleTextEditors.find(e => e.document.fileName === message.loc.file_name);
@@ -227,25 +226,33 @@ export class InfoProvider implements Disposable {
         }
         if (!editor) {return; }
         const pos = message.loc ? this.positionOfLocation(message.loc) : editor.selection.active;
-        const current_selection_range = editor.selection;
-        const cursor_pos = current_selection_range.active;
-        const prev_line = editor.document.lineAt(pos.line - 1);
-        const spaces = prev_line.firstNonWhitespaceCharacterIndex;
-        const margin_str = [...Array(spaces).keys()].map(x => ' ').join('');
+        const insert_type = message.insert_type ?? 'relative';
+        if (insert_type === 'relative') {
+            // in this case, assume that we actually want to insert at the same
+            // indentation level as the neighboring text
+            const current_selection_range = editor.selection;
+            const cursor_pos = current_selection_range.active;
+            const prev_line = editor.document.lineAt(pos.line - 1);
+            const spaces = prev_line.firstNonWhitespaceCharacterIndex;
+            const margin_str = [...Array(spaces).keys()].map(x => ' ').join('');
 
-        // [hack] for now, we assume that there is only ever one command per line
-        // and that the command should be inserted on the line above this one.
+            let new_command = message.text.replace(/\n/g, '\n' + margin_str);
+            new_command = `\n${margin_str}${new_command}`;
 
-        await editor.edit((builder) => {
-            builder.insert(
-                prev_line.range.end,
-                `\n${margin_str}${new_command}`);
-        });
-        editor.selection = new Selection(pos.line, spaces, pos.line, spaces);
+            await editor.edit((builder) => {
+                builder.insert(prev_line.range.end, new_command);
+            });
+            editor.selection = new Selection(pos.line, spaces, pos.line, spaces);
+        } else {
+            await editor.edit((builder) => {
+                builder.insert(pos, message.text);
+            });
+            editor.selection = new Selection(pos, pos)
+        }
     }
 
     private positionOfLocation(l: Location): Position {
-        return new Position(l.line - 1, l.column);
+        return new Position(l.line - 1, l.column ?? 0);
     }
     private makeLocation(file_name: string, pos: Position): Location {
         return {

src/shared.ts

@@ -70,6 +70,7 @@ export interface InsertTextMessage {
     /** If no location is given set to be the cursor position. */
     loc?: Location;
     text: string;
+    insert_type: 'absolute' | 'relative';
 }
 export interface RevealMessage {
     command: 'reveal';