message: replace till end of line
diff: -import { commands, Disposable, window, TextEditor, TextEditorEdit } from 'vscode';
  +import { commands, Disposable, window, TextEditor, TextEditorEdit, Position, Range } from 'vscode';
  import { Server } from './server';
  +import { Message } from 'lean-client-js-node';
  /** Pastes suggestions provided by tactics such as `squeeze_simp` */
  export class TacticSuggestions implements Disposable {
  @@ -10,15 +11,23 @@ export class TacticSuggestions implements Disposable {
  const commandHandler = (textEditor : TextEditor, edit : TextEditorEdit) => {
  const curFileName = textEditor.document.fileName;
  const curPosition = textEditor.selection.active;
  - const curSelection = textEditor.selection;
  + // Find message closest to the cursor
  const messages = this.server.messages
  - .filter((m) => m.file_name === curFileName &&
  - m.pos_line === curPosition.line + 1)
  - .sort((a, b) => a.pos_col - b.pos_col);
  + .filter((m : Message) => m.file_name === curFileName &&
  + m.pos_line === curPosition.line + 1 &&
  + m.pos_col <= curPosition.character)
  + .sort((a, b) => b.pos_col - a.pos_col);
  - if (messages.length > 0) {
  - edit.replace(curSelection, messages[0].text);
  - }
  + if (messages.length === 0) return;
  +
  + // Replace everything from the message start till the end of line
  + const msg = messages[0];
  + const range = new Range(
  + new Position(curPosition.line, msg.pos_col),
  + new Position(curPosition.line,
  + textEditor.document.lineAt(curPosition.line).range.end.character)
  + )
  + edit.replace(range, msg.text);
  };
  this.subscriptions.push(
  