From b4dd8db23fb09de21c1641d7c90b45dc6b7de626 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Sun, 15 Nov 2020 22:40:18 +0000 Subject: [PATCH 1/2] Add widget effect support for specifying location of text to insert. --- infoview/widget.tsx | 16 ++++++++++++++-- src/infoview.ts | 12 ++++-------- 2 files changed, 18 insertions(+), 10 deletions(-) diff --git a/infoview/widget.tsx b/infoview/widget.tsx index 7635895..73ddcfa 100644 --- a/infoview/widget.tsx +++ b/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; line_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,7 +82,19 @@ 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}; + let line = widget.line; + if (effect.line_type && effect.line) { + if (effect.line_type === 'relative') { + line = widget.line + effect.line; + } else { + line = effect.line + } + } + const loc = { + file_name, + line, + column: widget.column + }; edit(loc, effect.text); break; case 'reveal_position': reveal({file_name: effect.file_name || file_name, line: effect.line, column: effect.column}); break; diff --git a/src/infoview.ts b/src/infoview.ts index 6928681..bb65645 100644 --- a/src/infoview.ts +++ b/src/infoview.ts @@ -215,7 +215,7 @@ export class InfoProvider implements Disposable { this.proxyConnection.send(JSON.parse(message.payload)); } private async handleInsertText(message: InsertTextMessage) { - const new_command = message.text; + let new_command = message.text; let editor: TextEditor = null; if (message.loc) { editor = window.visibleTextEditors.find(e => e.document.fileName === message.loc.file_name); @@ -232,14 +232,10 @@ export class InfoProvider implements Disposable { 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. - + new_command = new_command.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}`); + builder.insert(prev_line.range.end, new_command); }); editor.selection = new Selection(pos.line, spaces, pos.line, spaces); } From 0315ed466657a6ff76f90766fb1ca21c717641e4 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Mon, 16 Nov 2020 10:58:24 +0000 Subject: [PATCH 2/2] Add support for absolute position insert_text. --- infoview/server.ts | 8 ++++---- infoview/widget.tsx | 23 +++++++++-------------- src/infoview.ts | 37 ++++++++++++++++++++++++------------- src/shared.ts | 1 + 4 files changed, 38 insertions(+), 31 deletions(-) diff --git a/infoview/server.ts b/infoview/server.ts index 7110aa4..cd59a78 100644 --- a/infoview/server.ts +++ b/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 { diff --git a/infoview/widget.tsx b/infoview/widget.tsx index 73ddcfa..e713dbc 100644 --- a/infoview/widget.tsx +++ b/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, line?: number; line_type?: 'relative' | 'absolute'} +| {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,20 +82,15 @@ export type WidgetEffect = function applyWidgetEffect(widget: WidgetIdentifier, file_name: string, effect: WidgetEffect) { switch (effect.kind) { case 'insert_text': - let line = widget.line; - if (effect.line_type && effect.line) { - if (effect.line_type === 'relative') { - line = widget.line + effect.line; - } else { - line = effect.line - } + 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}`); } - const loc = { - file_name, - line, - column: widget.column - }; - edit(loc, effect.text); 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; diff --git a/src/infoview.ts b/src/infoview.ts index bb65645..5228c96 100644 --- a/src/infoview.ts +++ b/src/infoview.ts @@ -215,7 +215,6 @@ export class InfoProvider implements Disposable { this.proxyConnection.send(JSON.parse(message.payload)); } private async handleInsertText(message: InsertTextMessage) { - let new_command = message.text; let editor: TextEditor = null; if (message.loc) { editor = window.visibleTextEditors.find(e => e.document.fileName === message.loc.file_name); @@ -227,21 +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(''); - new_command = new_command.replace(/\n/g, '\n' + margin_str); - new_command = `\n${margin_str}${new_command}`; - await editor.edit((builder) => { - builder.insert(prev_line.range.end, new_command); - }); - editor.selection = new Selection(pos.line, spaces, pos.line, spaces); + 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(''); + + 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, 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 { diff --git a/src/shared.ts b/src/shared.ts index 06235e0..abd90de 100644 --- a/src/shared.ts +++ b/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';