(WIP) add insertGoal command

infoview/info.tsx

@@ -1,6 +1,6 @@
 import { Location } from '../src/shared';
 import * as React from 'react';
-import { post, CopyToCommentEvent, copyToComment, PauseEvent, ContinueEvent, ToggleUpdatingEvent, global_server, ServerRestartEvent, AllMessagesEvent, currentAllMessages } from './server';
+import { post, CopyToCommentEvent, InsertFirstGoalEvent, copyToComment, PauseEvent, ContinueEvent, ToggleUpdatingEvent, global_server, ServerRestartEvent, AllMessagesEvent, currentAllMessages, edit } from './server';
 import { LocationContext, ConfigContext } from '.';
 import { Widget } from './widget';
 import { Goal } from './goal';
@@ -9,6 +9,7 @@ import { basename, useEvent } from './util';
 import { CopyToCommentIcon, PinnedIcon, PinIcon, ContinueIcon, PauseIcon, RefreshIcon, GoToFileIcon } from './svg_icons';
 import { Details } from './collapsing';
 import { Event, InfoResponse, CurrentTasksResponse, Message } from 'lean-client-js-core';
+import { match } from 'assert';
 
 /** Older versions of Lean can't deal with multiple simul info requests so this just prevents that. */
 class OneAtATimeDispatcher {
@@ -156,10 +157,16 @@ export function Info(props: InfoProps): JSX.Element {
         const goal = info.record && info.record.state;
         if (goal) copyToComment(goal);
     }
+    const matchFirstGoal = new RegExp(/^⊢ (([^\n]+\n)+[^\n]+)\n\n/m);
+    function insertFirstGoal() {
+        const goal = info.record && info.record.state;
+        if (goal) edit(loc, matchFirstGoal.exec(goal)[1]);
+    }
 
     // If we are the cursor infoview, then we should subscribe to
     // some commands from the extension
     useEvent(CopyToCommentEvent, () => isCursor && copyGoalToComment(), [isCursor, info]);
+    useEvent(InsertFirstGoalEvent, () => isCursor && insertFirstGoal(), [isCursor, info]);
     useEvent(PauseEvent, () => isCursor && setPaused(true), [isCursor]);
     useEvent(ContinueEvent, () => isCursor && setPaused(false), [isCursor]);
     useEvent(ToggleUpdatingEvent, () => isCursor && setPaused(!isCurrentlyPaused.current), [isCursor]);

infoview/server.ts

@@ -22,7 +22,7 @@ export function edit(loc: Location, text: string): void {
 }
 
 export function copyText(text: string): void {
-    post({ command: 'copy_text', text});
+    post({ command: 'copy_text', text });
 }
 
 export const PositionEvent: Event<Location> = new Event();
@@ -40,6 +40,7 @@ export const PauseEvent: Event<unknown> = new Event();
 export const ContinueEvent: Event<unknown> = new Event();
 export const ToggleUpdatingEvent: Event<unknown> = new Event();
 export const CopyToCommentEvent: Event<unknown> = new Event();
+export const InsertFirstGoalEvent: Event<unknown> = new Event();
 export const TogglePinEvent: Event<unknown> = new Event();
 export const ServerRestartEvent: Event<unknown> = new Event();
 export const AllMessagesEvent: Event<Message[]> = new Event();
@@ -62,6 +63,7 @@ window.addEventListener('message', event => { // messages from the extension
         case 'continue': ContinueEvent.fire(message); break;
         case 'toggle_updating': ToggleUpdatingEvent.fire(message); break;
         case 'copy_to_comment': CopyToCommentEvent.fire(message); break;
+        case 'insert_first_goal': InsertFirstGoalEvent.fire(message); break;
         case 'toggle_pin': TogglePinEvent.fire(message); break;
         case 'restart': ServerRestartEvent.fire(message); break;
         case 'all_messages': AllMessagesEvent.fire(message.messages); break;
@@ -125,4 +127,4 @@ global_server.logMessagesToConsole = true;
 global_server.allMessages.on(x => AllMessagesEvent.fire(x.msgs));
 global_server.connect();
 
-post({command:'request_config'});
+post({command:'request_config'});

package.json

@@ -220,6 +220,12 @@
 					"light": "./media/copy-to-comment-light.svg"
 				}
 			},
+			{
+				"command": "lean.infoView.insertFirstGoal",
+				"category": "Lean",
+				"title": "Info View: Insert First Goal",
+				"description": "Insert the first goal in the currently active tactic state widget at the cursor position."
+			},
 			{
 				"command": "lean.infoView.toggleStickyPosition",
 				"category": "Lean",

src/infoview.ts

@@ -100,6 +100,9 @@ export class InfoProvider implements Disposable {
             commands.registerTextEditorCommand('lean.infoView.copyToComment',() =>
                 this.postMessage({ command: 'copy_to_comment' })
             ),
+            commands.registerTextEditorCommand('lean.infoView.insertFirstGoal',() =>
+                this.postMessage({ command: 'insert_first_goal' })
+            ),
             commands.registerCommand('lean.infoView.toggleUpdating', () => this.postMessage({ command: 'toggle_updating' })),
             commands.registerTextEditorCommand('lean.infoView.toggleStickyPosition', () => this.postMessage({ command: 'toggle_pin' })),
         );
@@ -225,7 +228,7 @@ export class InfoProvider implements Disposable {
                 editor = window.visibleTextEditors[0];
             }
         }
-        if (!editor) {return; }
+        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;

src/shared.ts

@@ -109,4 +109,4 @@ export type ToInfoviewMessage =
     | { command: 'all_messages'; messages: Message[]}
     | { command: 'toggle_all_messages' }
     | SyncPinMessage
-    | { command: 'pause' | 'continue' | 'toggle_updating' | 'copy_to_comment' | 'toggle_pin' | 'restart'}
+    | { command: 'pause' | 'continue' | 'toggle_updating' | 'copy_to_comment' | 'insert_first_goal' | 'toggle_pin' | 'restart'}