From e930bbb8af850944f15f4206eb15616171cda5e9 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 25 Jan 2023 17:25:12 +0100
Subject: [PATCH] show unsolved goals message, but without the goals

---
 client/src/components/infoview/messages.tsx | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx
index c999ea5..2aee9b5 100644
--- a/client/src/components/infoview/messages.tsx
+++ b/client/src/components/infoview/messages.tsx
@@ -31,9 +31,12 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
     const title = `Line ${line+1}, Character ${character}`;
 
     // Hide "unsolved goals" messages
+    let message;
     if ("append" in diag.message && "text" in diag.message.append[0] &&
       diag.message?.append[0].text === "unsolved goals") {
-        return <></>
+        message = diag.message.append[0]
+    } else {
+        message = diag.message
     }
 
     return (
@@ -55,7 +58,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         <div className={severityClass + ' ml1 message'}>
             <p className="mv2">{title}</p>
             <pre className="font-code pre-wrap">
-                <InteractiveMessage fmt={diag.message} />
+                <InteractiveMessage fmt={message} />
             </pre>
         </div>
     // </details>