diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx index bf1e8fc..60a0229 100644 --- a/client/src/components/infoview/messages.tsx +++ b/client/src/components/infoview/messages.tsx @@ -10,6 +10,7 @@ import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/co import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer'; import { getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api'; import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; +import { InputModeContext } from '../Level'; interface MessageViewProps { uri: DocumentUri; @@ -39,6 +40,8 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => { message = diag.message } + const { commandLineMode } = React.useContext(InputModeContext) + return ( //
// {title} @@ -56,7 +59,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => { // //
-

{title}

+ {!commandLineMode &&

{title}

}