From cda4e5b859146648dbd00543e1dcb8a45e84a0f0 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 25 Jan 2023 16:36:21 +0100
Subject: [PATCH] Hide "unsolved goals" messages

---
 client/src/components/infoview/messages.tsx | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx
index fed7b7a..c999ea5 100644
--- a/client/src/components/infoview/messages.tsx
+++ b/client/src/components/infoview/messages.tsx
@@ -28,7 +28,14 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         [DiagnosticSeverity.Information]: 'information',
         [DiagnosticSeverity.Hint]: 'hint',
     }[diag.severity] : '';
-    const title = `${fname}:${line+1}:${character}`;
+    const title = `Line ${line+1}, Character ${character}`;
+
+    // Hide "unsolved goals" messages
+    if ("append" in diag.message && "text" in diag.message.append[0] &&
+      diag.message?.append[0].text === "unsolved goals") {
+        return <></>
+    }
+
     return (
     // <details open>
         // <summary className={severityClass + ' mv2 pointer'}>{title}