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}/>
)}
-
- {/*
- Messages ({messages.length})
*/}
+ {/*
+
+ Messages ({messages.length})
- {/* */}
-
+
+
*/}
{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 =
}
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 (
-
+ {/*
All Messages ({diags.length})
@@ -139,9 +139,9 @@ export function AllMessages({uri: uri0}: { uri: DocumentUri }) {
title={isPaused ? 'continue updating' : 'pause updating'}>
-
+ */}
-
+ {/* */}
)
}