phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Hide "unsolved goals" messages

Browse Source
This commit is contained in:
Alexander Bentkamp
2023-01-25 16:36:21 +01:00
parent 5bfae3a1c2
commit cda4e5b859
1 changed files with 8 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/infoview/messages.tsx
+8 -1
View File
@@ -28,7 +28,14 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
[DiagnosticSeverity.Information]: 'information', [DiagnosticSeverity.Information]: 'information',
[DiagnosticSeverity.Hint]: 'hint', [DiagnosticSeverity.Hint]: 'hint',
}[diag.severity] : ''; }[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 ( return (
// <details open> // <details open>
// <summary className={severityClass + ' mv2 pointer'}>{title} // <summary className={severityClass + ' mv2 pointer'}>{title}