Do not use half-formatted goals when copying to comment.

Author: gebner

infoview/goal.tsx

@@ -7,6 +7,21 @@ interface GoalProps {
     plainGoals: PlainGoal;
 }
 
+export function getGoals(plainGoals: PlainGoal): string[] {
+    if (plainGoals.goals) return plainGoals.goals
+    const goals: string[] = [];
+    const r = /```lean\n([^`]*)```/g
+    let match: RegExpExecArray
+    const unformatted = plainGoals.rendered;
+    do {
+        match = r.exec(unformatted)
+        if (match) {
+            goals.push(match[1])
+        }
+    } while (match)
+    return goals;
+}
+
 function emphasizeMessage(goal: string): string {
     return goal
         .replace(/([^`~@$%^&*()-=+\[{\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\|;:",.\/\s]+)✝([¹²³⁴-⁹⁰]*)/g, '<span class="goal-inaccessible">$1$2</span>')
@@ -21,19 +36,7 @@ export function Goal({plainGoals}: GoalProps): JSX.Element {
     const [filterIndex, setFilterIndex] = React.useState<number>(config.filterIndex ?? -1);
     if (!plainGoals) return null;
 
-    let goals = plainGoals.goals;
-    if (!goals) {
-        goals = [];
-        const r = /```lean\n([^`]*)```/g
-        let match: RegExpExecArray
-        const unformatted = plainGoals.rendered;
-        do {
-            match = r.exec(unformatted)
-            if (match) {
-                goals.push(match[1])
-            }
-        } while (match)
-    }
+    let goals = getGoals(plainGoals);
 
     if (!(reFilters.length === 0 || filterIndex === -1)) {
         goals = goals.map((g) =>

infoview/info.tsx

@@ -1,7 +1,7 @@
 import * as React from 'react';
 import { copyToCommentEvent, copyToComment, pauseEvent, continueEvent, toggleUpdating, serverRestarted, allMessagesEvent, requestPlainGoal, reveal, progressEvent } from './server';
 import { LocationContext, ConfigContext } from '.';
-import { Goal } from './goal';
+import { getGoals, Goal } from './goal';
 import { Messages, processMessages, ProcessedMessage, getMessagesFor } from './messages';
 import { basename, useEvent } from './util';
 import { CopyToCommentIcon, PinnedIcon, PinIcon, ContinueIcon, PauseIcon, RefreshIcon, GoToFileIcon } from './svg_icons';
@@ -120,7 +120,9 @@ export function Info(props: InfoProps): JSX.Element {
     const {loc, goal, error, loading, messages} = stateRef.current;
 
     function copyGoalToComment() {
-        if (goal?.rendered) void copyToComment(goal.rendered);
+        if (goal) {
+            void copyToComment(getGoals(goal).join('\n\n'));
+        }
     }
 
     // If we are the cursor infoview, then we should subscribe to