From 45bdc22600ba4ca0307259c314b365d65fc6a1e8 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Tue, 24 Jan 2023 10:50:51 +0100
Subject: [PATCH] show all messages, independent of cursor position

---
 client/src/components/infoview/info.tsx     | 10 +++++-----
 client/src/components/infoview/main.tsx     |  6 +++---
 client/src/components/infoview/messages.tsx |  6 +++---
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx
index b344be4..9745245 100644
--- a/client/src/components/infoview/info.tsx
+++ b/client/src/components/infoview/info.tsx
@@ -128,14 +128,14 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     selectedLocations={selectedLocs} widget={widget}/>
             </details>
         )}
-        <div style={{display: hasMessages ? 'block' : 'none'}} key='messages'>
-            {/* <details key='messages' open>
-                <summary className='mv2 pointer'>Messages ({messages.length})</summary> */}
+        {/* <div style={{display: hasMessages ? 'block' : 'none'}} key='messages'>
+            <details key='messages' open>
+                <summary className='mv2 pointer'>Messages ({messages.length})</summary>
                 <div className='ml1'>
                     <MessagesList uri={pos.uri} messages={messages} />
                 </div>
-            {/* </details> */}
-        </div>
+            </details>
+        </div> */}
         {nothingToShow && (
             isPaused ?
                 /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index 892d584..0623b3f 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -13,7 +13,7 @@ import './infoview.css'
 import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api';
 
 import { Infos } from './infos';
-import { AllMessages, WithLspDiagnosticsContext } from '../../../../node_modules/lean4-infoview/src/infoview/messages';
+import { AllMessages, WithLspDiagnosticsContext } from './messages';
 import { useClientNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { WithRpcSessions } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
@@ -65,9 +65,9 @@ function Main(props: {}) {
     } else {
         ret = <div className="ma1">
             <Infos />
-            {/* {curUri && <div className="mv2">
+            {curUri && <div className="mv2">
                 <AllMessages uri={curUri} />
-            </div>} */}
+            </div>}
         </div>
     }
 
diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx
index f64b495..12bdaed 100644
--- a/client/src/components/infoview/messages.tsx
+++ b/client/src/components/infoview/messages.tsx
@@ -130,7 +130,7 @@ export function AllMessages({uri: uri0}: { uri: DocumentUri }) {
 
     return (
     <RpcContext.Provider value={rs}>
-    <Details setOpenRef={setOpenRef as any} initiallyOpen={!config.autoOpenShowsGoal}>
+    {/* <Details setOpenRef={setOpenRef as any} initiallyOpen={!config.autoOpenShowsGoal}>
         <summary className="mv2 pointer">
             All Messages ({diags.length})
             <span className="fr">
@@ -139,9 +139,9 @@ export function AllMessages({uri: uri0}: { uri: DocumentUri }) {
                    title={isPaused ? 'continue updating' : 'pause updating'}>
                 </a>
             </span>
-        </summary>
+        </summary> */}
         <AllMessagesBody uri={uri} messages={iDiags} />
-    </Details>
+    {/* </Details> */}
     </RpcContext.Provider>
     )
 }