show all messages, independent of cursor position

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'>
+        {/* <div style={{display: hasMessages ? 'block' : 'none'}} key='messages'>
-            {/* <details key='messages' open>
+            <details key='messages' open>
-                <summary className='mv2 pointer'>Messages ({messages.length})</summary> */}
+                <summary className='mv2 pointer'>Messages ({messages.length})</summary>
                 <div className='ml1'>
                     <MessagesList uri={pos.uri} messages={messages} />
                 </div>
-            {/* </details> */}
+            </details>
-        </div>
+        </div> */}
         {nothingToShow && (
             isPaused ?
                 /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */

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>
     }
 

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>
     )
 }