From 5025fa939b04fd2661ab0e7c71b0df948df13a6d Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 30 Jan 2023 15:18:06 +0100
Subject: [PATCH] show line numbers only in editor mode

---
 client/src/components/infoview/messages.tsx | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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 (
     // <details open>
         // <summary className={severityClass + ' mv2 pointer'}>{title}
@@ -56,7 +59,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         //     </span>
         // </summary>
         <div className={severityClass + ' ml1 message'}>
-            <p className="mv2">{title}</p>
+            {!commandLineMode && <p className="mv2">{title}</p>}
             <pre className="font-code pre-wrap">
                 <InteractiveMessage fmt={message} />
             </pre>